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

Theorem prth 550
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 439 . 2 |- (((ph -> ps) /\ (ch -> th)) -> (ph -> ps))
2 simpr 443 . 2 |- (((ph -> ps) /\ (ch -> th)) -> (ch -> th))
31, 2anim12d 543 1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 357
This theorem is referenced by:  mo 1844  2mo 1901  euind 2491  reuind 2502  reuss2 2894  opelopabt 3579  reusv3i 3834  tfrlem5 5323  rlimcn2 9176  o1of2 9183  o1rlimmul 9188  spanuni 13575  pm11.71 17557
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 175  df-an 359
Copyright terms: Public domain