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

Theorem prth 546
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 436 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  ( ph  ->  ps ) )
2 simpr 440 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  ( ch  ->  th ) )
31, 2anim12d 539 1  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  (
( ph  /\  ch )  ->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 356
This theorem is referenced by:  mo  1967  2mo  2024  euind  2632  reuind  2646  reuss2  3063  opelopabt  3826  reusv3i  4100  tfrlem5  5843  wemaplem2  6735  rlimcn2  10706  o1of2  10713  o1rlimmul  10718  2sqlem6  18083  spanuni  19439  pm11.71  24249
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 358
Copyright terms: Public domain