MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prth Unicode version

Theorem prth 548
Description: Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 540. 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 540 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  1975  2mo  2032  euind  2640  reuind  2654  reuss2  3071  opelopabt  3840  reusv3i  4114  tfrlem5  5861  wemaplem2  6755  rexanre  11041  rlimcn2  11275  o1of2  11297  o1rlimmul  11303  2sqlem6  19183  spanuni  20679  pm11.71  25470
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 W3C validator