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

Theorem prth 551
Description: Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 542. 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 439 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  ( ph  ->  ps ) )
2 simpr 443 . 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 5    /\ wa 357
This theorem is referenced by:  mo  2123  2mo  2179  euind  2874  reuind  2888  reuss2  3335  opelopabt  4149  reusv3i  4411  tfrlem5  6256  wemaplem2  7120  rexanre  11641  rlimcn2  11875  o1of2  11897  o1rlimmul  11903  2sqlem6  20258  spanuni  21754  pm11.71  26568
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9
This theorem depends on definitions:  df-bi 176  df-an 359
  Copyright terms: Public domain W3C validator