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

Theorem prth 554
Description: Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 546. 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 443 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  ( ph  ->  ps ) )
2 simpr 447 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  ( ch  ->  th ) )
31, 2anim12d 546 1  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  th ) )  ->  (
( ph  /\  ch )  ->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mo  2165  2mo  2221  euind  2952  reuind  2968  reuss2  3448  opelopabt  4277  reusv3i  4541  tfrlem5  6396  wemaplem2  7262  rexanre  11830  rlimcn2  12064  o1of2  12086  o1rlimmul  12092  2sqlem6  20608  spanuni  22123  pm11.71  27596
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 177  df-an 360
  Copyright terms: Public domain W3C validator