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

Theorem prth 642
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 507 . 2 |- (((ph -> ps) /\ (ch -> th)) -> (ph -> ps))
2 simpr 511 . 2 |- (((ph -> ps) /\ (ch -> th)) -> (ch -> th))
31, 2anim12d 633 1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 418
This theorem is referenced by:  anim12dOLD 775  mo 2004  2mo 2061  euind 2658  reuind 2669  reuss2 3059  opelopabt 3736  reusv3i 3991  tfrlem5 5443  cau3iri 9064  cvganz 9073  clm3i 9272  climunii 9291  climaddlem3 9313  climmullem8 9324  xplm 10838  xpcn 10839  lmcau 10859  hlimcauii 12218  hlimuniii 12220  spanuni 12576  pm11.71 16981
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 210  df-an 420
Copyright terms: Public domain