Return to Revisions

Hint

Assume S and derive R ∨ P from 1st premise.

Now two sub-proofs, for ∨-elim:

1. Assume R and derive Q ∨ R by ∨-intro, and it is done.

2. Assume P and derive ¬R → Q from 2nd premise.

Now use R ∨ ¬R (Excluded Middle) for a new ∨-elim:

2.1) Assume R and derive Q ∨ R.

2.2) Assume ¬R and derive Q from ¬R → Q and derive Q ∨ R.

Having derived Q ∨ R in each case, we can conclude with:

S → (Q ∨ R)

by →-intro.