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

Theorem prth 555
Description: Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 547. 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 444 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  ( ph  ->  ps ) )
2 simpr 448 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  ( ch  ->  th ) )
31, 2anim12d 547 1  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  (
( ph  /\  ch )  ->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mo  2276  2mo  2332  euind  3081  reuind  3097  reuss2  3581  opelopabt  4427  reusv3i  4689  tfrlem5  6600  wemaplem2  7472  rexanre  12105  rlimcn2  12339  o1of2  12361  o1rlimmul  12367  2sqlem6  21106  spanuni  22999  pm11.71  27464
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 178  df-an 361
  Copyright terms: Public domain W3C validator