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

Theorem prth 556
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 443 . 2 |- (((ph -> ps) /\ (ch -> th)) -> (ph -> ps))
2 simpr 447 . 2 |- (((ph -> ps) /\ (ch -> th)) -> (ch -> th))
31, 2anim12d 549 1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 361
This theorem is referenced by:  mo 1850  2mo 1907  euind 2497  reuind 2508  reuss2 2900  opelopabt 3588  reusv3i 3843  tfrlem5 5347  rlimcn2 9199  o1of2 9206  o1rlimmul 9211  spanuni 13608  pm11.71 17590
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 363
Copyright terms: Public domain