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

Theorem prth 549
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). (Contributed by NM, 12-Aug-1993.) (Proof 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 437 . 2  |-  ( (
( ph  ->  ps )  /\  ( ch  ->  th )
)  ->  ( ph  ->  ps ) )
2 simpr 441 . 2  |-  ( (
( ph  ->  ps )  /\  ( ch  ->  th )
)  ->  ( ch  ->  th ) )
31, 2anim12d 542 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  1988  2mo  2045  euind  2652  reuind  2666  reuss2  3082  opelopabt  3844  reusv3i  4118  tfrlem5  5843  wemaplem2  6725  rlimcn2  10678  o1of2  10685  o1rlimmul  10690  2sqlem6  17992  spanuni  19344  pm11.71  24157
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