Theorem prth 556

Description: Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema.'

Assertion

Ref	Expression
prth	|- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))

Proof of Theorem prth

Step	Hyp	Ref	Expression
1		pm3.2 283	. . . . 5 |- (ps -> (th -> (ps /\ th)))
2	1	imim2d 25	. . . 4 |- (ps -> ((ch -> th) -> (ch -> (ps /\ th))))
3	2	imim2i 17	. . 3 |- ((ph -> ps) -> (ph -> ((ch -> th) -> (ch -> (ps /\ th)))))
4	3	com23 32	. 2 |- ((ph -> ps) -> ((ch -> th) -> (ph -> (ch -> (ps /\ th)))))
5	4	imp4b 365	1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anim12d 558  mo 1393  2mo 1447  reuss2 2275  ssxp 3256  tfrlem5 3915  cau3ir 6915  cvganz 6924  clm3 7079  climunii 7098  climaddlem3 7116  climmullem8 7127  xplm 7975  xpcn 7976  lmcau 7996  hlimcaui 9106  hlimunii 9108  spanun 9467

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain