Theorem prth 554

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 556  mo 1370  2mo 1424  reuss2 2246  ssxp 3218  tfrlem5 3854  cau3ir 6803  cvganz 6812  clm3 6968  climunii 6986  climaddlem3 7003  climmullem8 7014  xplm 7857  xpcn 7858  lmcau 7878  hlimcaui 9257  hlimunii 9259  spanun 9596

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