HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem prth 627
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
StepHypRef Expression
1 simpl 496 . 2 |- (((ph -> ps) /\ (ch -> th)) -> (ph -> ps))
2 simpr 500 . 2 |- (((ph -> ps) /\ (ch -> th)) -> (ch -> th))
31, 2anim12d 618 1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 412
This theorem is referenced by:  anim12dOLD 758  mo 1987  2mo 2044  euind 2641  reuind 2652  reuss2 3042  opelopabt 3719  reusv3i 3974  tfrlem5 5426  cau3iri 9049  cvganz 9058  clm3i 9257  climunii 9276  climaddlem3 9298  climmullem8 9309  xplm 10874  xpcn 10875  lmcau 10895  hlimcauii 12255  hlimuniii 12257  spanuni 12613  pm11.71 17203
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 204  df-an 414
Copyright terms: Public domain