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 1431  2mo 1486  reuss2 2326  ssxp 3344  tfrlem5 4214  cau3iri 7116  cvganz 7125  clm3i 7280  climunii 7299  climaddlem3 7317  climmullem8 7328  xplm 8184  xpcn 8185  lmcau 8205  hlimcauii 9376  hlimuniii 9378  spanuni 9737  heiborlem36 11939

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