Theorem prth 541

Description: Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema' (splendid theorem). (The proof was shortened by Wolf Lammen, 7-Apr-2013.)

Assertion

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

Proof of Theorem prth

Step	Hyp	Ref	Expression
1		simpl 437	. 2 |- (((ph -> ps) /\ (ch -> th)) -> (ph -> ps))
2		simpr 442	. 2 |- (((ph -> ps) /\ (ch -> th)) -> (ch -> th))
3	1, 2	anim12d 533	1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))

Syntax hints:   -> wi 3   /\ wa 337

This theorem is referenced by:  anim12dOLD 702  mo 2053  2mo 2110  euind 2685  reuind 2696  reuss2 3077  opelopabt 3727  reusv3i 3973  tfrlem5 5287  cau3iri 8552  cvganz 8561  clm3i 8735  climunii 8754  climaddlem3 8772  climmullem8 8783  xplm 10119  xpcn 10120  lmcau 10140  hlimcauii 11573  hlimuniii 11575  spanuni 11934  heiborlem36 16814  pm11.71 17178

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 220  df-an 339

Copyright terms: Public domain