*5·63. ⊢: . p ∨ q . ≡: p . ∨ . ∼ p . q {\displaystyle \scriptstyle {\vdash :.p\lor q.\equiv :p.\lor .\sim p.q}} [ ∗ 5 ⋅ 62 ∼ p , q q , p ] {\displaystyle \scriptstyle {\left[*5\cdot 62{\frac {\sim p,q}{q,~~p}}\right]}}
*5·7. ⊢: . p ∨ r . ≡ . q ∨ r :≡: r . ∨ . p ≡ q {\displaystyle \scriptstyle {\vdash :.p\lor r.\equiv .q\lor r:\equiv :r.\lor .p\equiv q}} [ ∗ 4 ⋅ 74. ∗ 1 ⋅ 3. ∗ 5 ⋅ 1. ∗ 4 ⋅ 37 ] {\displaystyle \scriptstyle {[*4\cdot 74.*1\cdot 3.*5\cdot 1.*4\cdot 37]}}
*5·71. ⊢: . q ⊃∼ r . ⊃: p ∨ q . r . ≡ . p . r {\displaystyle \scriptstyle {\vdash :.q\supset \sim r.\supset :p\lor q.r.\equiv .p.r}}
In the following proof, as always henceforth, " Hp {\displaystyle \scriptstyle {\text{Hp}}} " means the hypothesis of the proposition to be proved.
Dem.
⊢ . ∗ 4 ⋅ 4. ⊃⊢: . p ∨ q . r . ≡: p . r . ∨ . q . r (1) ⊢ . ∗ 4 ⋅ 62 ⋅ 51. ⊃⊢:: Hp . ⊃: . ∼ ( q . r ) : . [ ∗ 4 ⋅ 74 ] ⊃: . p . r . ∨ . q . r :≡: p . r (2) ⊢ . ( 1 ) . ( 2 ) . ∗ 4 ⋅ 22. ⊃⊢ . Prop {\displaystyle {\begin{array}{lllr}\scriptstyle {\vdash .*4\cdot 4.}&\scriptstyle {\supset \vdash :.p\lor q}&\scriptstyle {.r.\equiv :p.r.\lor .q.r}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\\scriptstyle {\vdash .*4\cdot 62\cdot 51.}&\scriptstyle {\supset \vdash ::{\text{Hp}}.}&\scriptstyle {\supset :.\sim (q.r):.}\\\scriptstyle {[*4\cdot 74]}&&\scriptstyle {\supset :.p.r.\lor .q.r:\equiv :p.r}&\scriptstyle {\text{(2)}}\\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {*4\cdot 22.\supset \vdash }&\scriptstyle {.{\text{Prop}}}\end{array}}}
*5·74. ⊢: . p . ⊃ . q ≡ r :≡: p ⊃ q . ≡ . p ⊃ r {\displaystyle \scriptstyle {\vdash :.p.\supset .q\equiv r:\equiv :p\supset q.\equiv .p\supset r}}
⊢ . ∗ 5 ⋅ 41. ⊃⊢:: p ⊃ q . ⊃ . p ⊃ r :≡: p . ⊃ . q ⊃ r : . p ⊃ r . ⊃ . p ⊃ q :≡: p . ⊃ . r ⊃ q (1) ⊢ . ( 1 ) . ∗ 4 ⋅ 38. ⊃⊢:: p ⊃ q . ≡ . p ⊃ r . ≡: . p . ⊃ . q ⊃ r : p . ⊃ . r ⊃ q : . [ ∗ 4 ⋅ 76 ] ≡: . p . ⊃ . q ≡ r ::⊃⊢ . Prop {\displaystyle {\begin{array}{lllr}\scriptstyle {\vdash .*5\cdot 41.\supset \vdash ::p\supset q.\supset .}&\scriptstyle {p\supset r:\equiv :p}&\scriptstyle {.\supset .q\supset r:.}\\&\scriptstyle {p\supset r.\supset .p}&\scriptstyle {\supset q:\equiv :p.\supset .r\supset q}&\scriptstyle {\qquad {\text{(1)}}}\\\scriptstyle {\vdash .(1).*4\cdot 38.\supset \vdash ::p\supset q.}&\scriptstyle {\equiv .p\supset r.}&\scriptstyle {\equiv :.p.\supset .q\supset r:p.\supset .r\supset q:.}\\\scriptstyle {[*4\cdot 76]}&&\scriptstyle {\equiv :.p.\supset .q\equiv r::\supset \vdash .{\text{Prop}}}\end{array}}}
*5·75. ⊢: . r ⊃∼ q : p . ≡ . q ∨ r :⊃: p . ∼ q . ≡ . r {\displaystyle \scriptstyle {\vdash :.r\supset \sim q:p.\equiv .q\lor r:\supset :p.\sim q.\equiv .r}}
⊢ . ∗ 5 ⋅ 6. ⊃⊢: . Hp . ⊃: p . ∼ q . ⊃ . r (1) ⊢ . ∗ 3 ⋅ 27. ⊃⊢: . Hp . ⊃: q ∨ r . ⊃ . p : [ ∗ 4 ⋅ 77 ] ⊃: r ⊃ p (2) ⊢ . ∗ 3 ⋅ 26. ⊃⊢: . Hp . ⊃: r ⊃∼ q (3) ⊢ . ( 2 ) . ( 3 ) . Comp . ⊃⊢: . Hp . ⊃: r ⊃ p . r ⊃∼ q : [ Comp ] ⊃: r . ⊃ . p . ∼ q (4) ⊢ . ( 1 ) . ( 4 ) . Comp . ⊃⊢: . Hp . ⊃: p . ∼ q . ≡ . r : . ⊃⊢ . Prop {\displaystyle {\begin{array}{llllr}\scriptstyle {\vdash .*5\cdot 6.}&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :p.\sim q}&\scriptstyle {.\supset .r}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\\scriptstyle {\vdash .*3\cdot 27.}&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :q\lor r.}&\scriptstyle {\supset .p:}\\\scriptstyle {[*4\cdot 77]}&&\scriptstyle {\supset :r\supset p}&&\scriptstyle {\text{(2)}}\\\scriptstyle {\vdash .*3\cdot 26.}&&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :r\supset \sim q}&\scriptstyle {\text{(3)}}\\\scriptstyle {\vdash .(2).(3)}&\scriptstyle {.{\text{Comp}}.}&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :r\supset p.r\supset \sim q:}\\\scriptstyle {[{\text{Comp}}]}&&\scriptstyle {\supset :r.\supset .p.\sim q}&&\scriptstyle {\text{(4)}}\\\scriptstyle {\vdash .(1).(4)}&\scriptstyle {.{\text{Comp}}.}&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :p.\sim q.\equiv .r:.\supset \vdash .{\text{Prop}}}\end{array}}}