Theorem prth 558

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 281	. . . . 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 363	1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  anim12d 560  mo 1430  2mo 1485  reuss2 2325  ssxp 3342  tfrlem5 4211  cau3iri 7106  cvganz 7115  clm3i 7270  climunii 7289  climaddlem3 7307  climmullem8 7318  xplm 8173  xpcn 8174  lmcau 8194  hlimcauii 9359  hlimuniii 9361  spanuni 9720

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 145  df-an 223

Copyright terms: Public domain