*2·68. ⊢: . p ⊃ q . ⊃ . q :⊃ . p ∨ q {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset .q:\supset .p\lor q}}
Dem.
[ ∗ 2 ⋅ 67 ∼ p p ] ⊢: . p ⊃ q . ⊃ . q :⊃ . ∼ p ⊃ q ( 1 ) ⊢ . ( 1 ) . ∗ 2 ⋅ 54. ⊃⊢ . Prop {\displaystyle {\begin{aligned}&\scriptstyle {\left[*2\cdot 67{\frac {\sim p}{p}}\right]\vdash :.p\supset q.\supset .q:\supset .\sim p\supset q\qquad \qquad \qquad (1)}\\&\scriptstyle {\vdash .(1).*2\cdot 54.\supset \vdash .{\text{Prop}}}\end{aligned}}}
*2·69. ⊢: . p ⊃ q . ⊃ . q :⊃: q ⊃ p . ⊃ . p [ ∗ 2 ⋅ 68. Perm . ∗ 2 ⋅ 62 q , p p , q ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset .q:\supset :q\supset p.\supset .p\qquad \left[*2\cdot 68.{\text{Perm}}.*2\cdot 62{\frac {q,p}{p,q}}\right]}}
*2·73. ⊢: . p ⊃ q . ⊃: p ∨ q ∨ r . ⊃ . q ∨ r [ ∗ 2 ⋅ 621 ⋅ 38 ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :p\lor q\lor r.\supset .q\lor r\qquad [*2\cdot 621\cdot 38]}}
*2·74. ⊢: . q ⊃ p . ⊃: p ∨ q ∨ r . ⊃ . p ∨ r [ ∗ 2 ⋅ 73 q , p p , q . Assoc . Syll ] {\displaystyle \scriptstyle {\vdash :.q\supset p.\supset :p\lor q\lor r.\supset .p\lor r\qquad \left[*2\cdot 73{\frac {q,p}{p,q}}.{\text{Assoc}}.{\text{Syll}}\right]}}
*2·75. ⊢:: p ∨ q . ⊃: . p . ∨ . q ⊃ r :⊃ . p ∨ r [ ∗ 2 ⋅ 74 ∼ q q . ∗ 2 ⋅ 53 ⋅ 31 ] {\displaystyle \scriptstyle {\vdash ::p\lor q.\supset :.p.\lor .q\supset r:\supset .p\lor r\qquad \left[*2\cdot 74{\frac {\sim q}{q}}.*2\cdot 53\cdot 31\right]}}
*2·76. ⊢: . p . ∨ . q ⊃ r :⊃: p ∨ q . ⊃ . p ∨ r [ ∗ 2 ⋅ 75. Comm ] {\displaystyle \scriptstyle {\vdash :.p.\lor .q\supset r:\supset :p\lor q.\supset .p\lor r\qquad [*2\cdot 75.{\text{Comm}}]}}
*2·77. ⊢: . p . ⊃ . q ⊃ r :⊃: p ⊃ q . ⊃ . p ⊃ r [ ∗ 2 ⋅ 76 ∼ p p ] {\displaystyle \scriptstyle {\vdash :.p.\supset .q\supset r:\supset :p\supset q.\supset .p\supset r\qquad \left[*2\cdot 76{\frac {\sim p}{p}}\right]}}
*2·8. ⊢: . q ∨ r . ⊃:∼ r ∨ s . ⊃ . q ∨ s {\displaystyle \scriptstyle {\vdash :.q\lor r.\supset :\sim r\lor s.\supset .q\lor s}}
⊢ . ∗ 2 ⋅ 53. Perm . ⊃⊢: . q ∨ r . ⊃:∼ r ⊃ q : [ ∗ 2 ⋅ 38 ] ⊃:∼ r ∨ s . ⊃ . q ∨ s : . ⊃⊢ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .*2\cdot 53.{\text{Perm}}.\supset \vdash :.q\lor r.}&\scriptstyle {\supset :\sim r\supset q:}\\\scriptstyle {[*2\cdot 38]}&\scriptstyle {\supset :\sim r\lor s.\supset .q\lor s:.\supset \vdash .{\text{Prop}}}\end{array}}}
*2·81. ⊢:: q . ⊃ . r ⊃ s :⊃: . p ∨ q . ⊃: p ∨ r . ⊃ . p ∨ s {\displaystyle \scriptstyle {\vdash ::q.\supset .r\supset s:\supset :.p\lor q.\supset :p\lor r.\supset .p\lor s}}
⊢ . Sum . ⊃⊢:: q . ⊃ . r ⊃ s :⊃: . p ∨ q . ⊃: p . ∨ . r ⊃ s ( 1 ) ⊢ . ∗ 2 ⋅ 76. Syll . ⊃⊢:: p ∨ q . ⊃: p . ∨ . r ⊃ s : . ⊃: . p ∨ q . ⊃: p ∨ r . ⊃ . p ∨ s ( 2 ) ⊢ . ( 1 ) . ( 2 ) . ⊃⊢ . Prop {\displaystyle {\begin{array}{lll}\scriptstyle {\vdash .{\text{Sum}}.\supset \vdash ::q.\supset .r\supset s:\supset :.p\lor }&\scriptstyle {q.\supset :p.\lor .r\supset s\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {\vdash .*2\cdot 76.{\text{Syll}}.\supset \vdash ::p\lor q.\supset :p.\lor }&\scriptstyle {.r\supset s:.\supset :.}\\&\scriptstyle {p\lor q.\supset :p\lor r.\supset .p\lor s}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(1).(2).\supset \vdash .{\text{Prop}}}\end{array}}}
*2·82. ⊢: . p ∨ q ∨ r . ⊃: p ∨ ∼ r ∨ s . ⊃ . p ∨ q ∨ s [ ∗ 2 ⋅ 8. ∗ 2 ⋅ 81 q ∨ r , ∼ r ∨ s , q ∨ s q , r , s ] {\displaystyle {\begin{aligned}\scriptstyle {\vdash :.p\lor q\lor r.\supset :p\lor \sim r\lor s.\supset .p\lor }&\scriptstyle {q\lor s}\\&\scriptstyle {\left[*2\cdot 8.*2\cdot 81{\frac {q\lor r,\sim r\lor s,q\lor s}{q,\quad r,\quad s}}\right]}\end{aligned}}}
*2·83. ⊢:: p . ⊃ . q ⊃ r :⊃: . p . ⊃ . r ⊃ s : ⊃: p . ⊃ . q ⊃ s [ ∗ 2 ⋅ 82 ∼ p , ∼ q p , q ] {\displaystyle {\begin{aligned}\scriptstyle {\vdash ::p.\supset .q\supset r:\supset :.p.\supset .r\supset s:}&\scriptstyle {\supset :p.\supset .q\supset s}\\&\scriptstyle {\left[*2\cdot 82{\frac {\sim p,\sim q}{p,~~q}}\right]}\end{aligned}}}
*2·85. ⊢: . p ∨ q . ⊃ . p ∨ r :⊃: p . ∨ . q ⊃ r {\displaystyle \scriptstyle {\vdash :.p\lor q.\supset .p\lor r:\supset :p.\lor .q\supset r}}
[ Add . Syll ] ⊢: . p ∨ q . ⊃ . r :⊃ . q ⊃ r ( 1 ) ⊢ . ∗ 2 ⋅ 55. ⊃ ⊢::∼ p . ⊃: . p ∨ r . ⊃ . r : . [ Syll ] ⊃: . p ∨ q . ⊃ . p ∨ r : ⊃: p ∨ q . ⊃ . r : . [ ( 1 ) . ∗ 2 ⋅ 83 ] ⊃: . p ∨ q . ⊃ . p ∨ r : ⊃: q ⊃ r ( 2 ) ⊢ . ( 2 ) . Com m . ⊃⊢: . p ∨ q . ⊃ . p ∨ r : ⊃:∼ p . ⊃ . q ⊃ r : [ ∗ 2 ⋅ 54 ] ⊃: p . ∨ . q ⊃ r : . ⊃⊢ . Prop {\displaystyle {\begin{array}{lllll}\scriptstyle {[{\text{Add}}.{\text{Syll}}]}&\scriptstyle {\vdash :.p\lor q}&\scriptstyle {.\supset .r:\supset .q\supset r}&&\scriptstyle {(1)}\\\scriptstyle {\vdash .*2\cdot 55.\supset }&\scriptstyle {\vdash ::\sim p.}&\scriptstyle {\supset :.p\lor r.\supset .r:.}\\\scriptstyle {[{\text{Syll}}]}&&\scriptstyle {\supset :.p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :p\lor q.\supset .r:.}\\\scriptstyle {[(1).*2\cdot 83]}&&\scriptstyle {\supset :.p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :q\supset r}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(2).{\text{Com}}}&\scriptstyle {{\text{m}}.\supset \vdash :.}&\scriptstyle {\quad p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :\sim p.\supset .q\supset r:}\\\scriptstyle {[*2\cdot 54]}&&&\scriptstyle {\supset :p.\lor .q\supset r:.\supset \vdash .}&\scriptstyle {\text{Prop}}\end{array}}}
*2·86. ⊢: . p ⊃ q . ⊃ . p ⊃ r :⊃: p . ⊃ . q ⊃ r [ ∗ 2 ⋅ 85 ∼ p p ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset .p\supset r:\supset :p.\supset .q\supset r\quad \left[*2\cdot 85{\frac {\sim p}{p}}\right]}}