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 3587  reusv3i 3842  tfrlem5 5332  rlimcn2 9184  o1of2 9191  o1rlimmul 9196  spanuni 13586  pm11.71 17568
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