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

Theorem imim12d 68
Description: Deduction combining antecedents and consequents. (Contributed by NM, 7-Aug-1994.) (Proof shortened by O'Cat, 30-Oct-2011.)
Hypotheses
Ref Expression
imim12d.1  |-  ( ph  ->  ( ps  ->  ch ) )
imim12d.2  |-  ( ph  ->  ( th  ->  ta ) )
Assertion
Ref Expression
imim12d  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  ta ) ) )

Proof of Theorem imim12d
StepHypRef Expression
1 imim12d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 imim12d.2 . . 3  |-  ( ph  ->  ( th  ->  ta ) )
32imim2d 48 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ch  ->  ta ) ) )
41, 3syl5d 62 1  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1d  69  equveli  1928  mo  2165  rspcimdv  2885  peano5  4679  tfrlem1  6391  isf34lem6  8006  inar1  8397  supsrlem  8733  uzindOLD  10106  r19.29uz  11834  o1of2  12086  o1rlimmul  12092  caucvg  12151  isprm5  12791  mrissmrid  13543  kgen2ss  17250  txlm  17342  isr0  17428  metcnpi3  18092  addcnlem  18368  nmhmcn  18601  aalioulem5  19716  xrlimcnp  20263  dmdmd  22880  mdsl0  22890  mdsl1i  22901  ghomf1olem  23412  ax13dfeq  23566  ispridlc  26107  infrglb  27134  bnj517  28290  a12lem1  28503
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator