*3·45. ⊢: . p ⊃ q . ⊃: p . r . ⊃ . q . r {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :p.r.\supset .q.r}}
This principle shows that we may multiply both sides of an implication by a common factor; hence it is called by Peano the "principle of the factor." We shall refer to it as "Fact." It is the analogue, for multiplication, of the primitive proposition *1·6 .
Dem.
⊢ . Syll ∼ r r . ⊃⊢: . p ⊃ q . ⊃: q ⊃∼ r . ⊃ . p ⊃∼ r : [ Transp ] ⊃:∼ ( p ⊃∼ r ) . ⊃ . ∼ ( q ⊃∼ r ) : . [ Id . ( ∗ 1 ⋅ 01. ∗ 3 ⋅ 01 ) ] ⊃⊢ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{ll}\scriptstyle {\vdash .{\text{Syll}}{\frac {\sim r}{r}}.\supset \vdash :.p\supset q.}&\scriptstyle {\supset :q\supset \sim r.\supset .p\supset \sim r:}\\\scriptstyle {[{\text{Transp}}]}&\scriptstyle {\supset :\sim (p\supset \sim r).\supset .\sim (q\supset \sim r):.}\end{array}}\\&\scriptstyle {~[{\text{Id}}.(*1\cdot 01.*3\cdot 01)]\supset \vdash .{\text{Prop}}}\end{aligned}}}
*3·47. ⊢: . p ⊃ r . q ⊃ s . ⊃: p . q . ⊃ . r . s {\displaystyle \scriptstyle {\vdash :.p\supset r.q\supset s.\supset :p.q.\supset .r.s}}
This proposition, or rather its analogue for classes, was proved by Leibniz, and evidently pleased him, since he calls it "præclarum theorema[1] ."
Dem.
⊢ . ∗ 3 ⋅ 26. ⊃⊢: . p ⊃ r . q ⊃ s . ⊃: p ⊃ r : [ Fact ] ⊃: p . q . ⊃ . r . q : [ ∗ 3 ⋅ 22 ] ⊃: p . q . ⊃ . q . r ( 1 ) ⊢ . ∗ 3 ⋅ 27. ⊃⊢: . p ⊃ r . q ⊃ s . ⊃: q ⊃ s : [ Fact ] ⊃: q . r . ⊃ . s . r : [ ∗ 3 ⋅ 22 ] ⊃: q . r . ⊃ . r . s ( 2 ) ⊢ . ( 1 ) . ( 2 ) . ∗ 3 ⋅ 03. ∗ 2 ⋅ 83. ⊃ ⊢: . p ⊃ r . q ⊃ s . ⊃: p . q . ⊃ . r . s : . ⊃⊢ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{llr}\scriptstyle {\vdash .*3\cdot 26.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :p\supset r:}\\\scriptstyle {[{\text{Fact}}]}&\scriptstyle {\supset :p.q.\supset .r.q:}\\\scriptstyle {[*3\cdot 22]}&\scriptstyle {\supset :p.q.\supset .q.r\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {\vdash .*3\cdot 27.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :q\supset s:}\\\scriptstyle {[{\text{Fact}}]}&\scriptstyle {\supset :q.r.\supset .s.r:}\\\scriptstyle {[*3\cdot 22]}&\scriptstyle {\supset :q.r.\supset .r.s}&\scriptstyle {(2)}\end{array}}\\&\scriptstyle {~\vdash .(1).(2).*3\cdot 03.*2\cdot 83.\supset }\\&\scriptstyle {\qquad \qquad \vdash :.p\supset r.q\supset s.\supset :p.q.\supset .r.s:.\supset \vdash .{\text{Prop}}}\end{aligned}}}
*3·48. ⊢: . p ⊃ r . q ⊃ s . ⊃: p ∨ q . ⊃ . r ∨ s {\displaystyle \scriptstyle {\vdash :.p\supset r.q\supset s.\supset :p\lor q.\supset .r\lor s}}
This theorem is the analogue of *3·47.
Dem.
⊢ . ∗ 3 ⋅ 26. ⊃⊢: . p ⊃ r . q ⊃ s . ⊃: p ⊃ r : [ Sum ] ⊃: p ∨ q . ⊃ . r ∨ q : [ Perm ] ⊃: p ∨ q . ⊃ . q ∨ r ( 1 ) ⊢ . ∗ 3 ⋅ 27. ⊃⊢: . p ⊃ r . q ⊃ s . ⊃: q ⊃ s : [ Sum ] ⊃: q ∨ r . ⊃ . s ∨ r : [ Perm ] ⊃: q ∨ r . ⊃ . r ∨ s ( 2 ) ⊢ . ( 1 ) . ( 2 ) . ∗ 2 ⋅ 83. ⊃ ⊢: . p ⊃ r . q ⊃ s . ⊃: p ∨ q . ⊃ . r ∨ s : . ⊃⊢ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{llr}\scriptstyle {\vdash .*3\cdot 26.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :p\supset r:}\\\scriptstyle {[{\text{Sum}}]}&\scriptstyle {\supset :p\lor q.\supset .r\lor q:}\\\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\supset :p\lor q.\supset .q\lor r\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {\vdash .*3\cdot 27.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :q\supset s:}\\\scriptstyle {[{\text{Sum}}]}&\scriptstyle {\supset :q\lor r.\supset .s\lor r:}\\\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\supset :q\lor r.\supset .r\lor s}&\scriptstyle {(2)}\end{array}}\\&\scriptstyle {~\vdash .(1).(2).*2\cdot 83.\supset }\\&\scriptstyle {\qquad \qquad \vdash :.p\supset r.q\supset s.\supset :p\lor q.\supset .r\lor s:.\supset \vdash .{\text{Prop}}}\end{aligned}}}
↑ Philosophical works , Gerhardt's edition, Vol. vii . p. 223.