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  1941  mo  2178  rspcimdv  2898  peano5  4695  tfrlem1  6407  isf34lem6  8022  inar1  8413  supsrlem  8749  uzindOLD  10122  r19.29uz  11850  o1of2  12102  o1rlimmul  12108  caucvg  12167  isprm5  12807  mrissmrid  13559  kgen2ss  17266  txlm  17358  isr0  17444  metcnpi3  18108  addcnlem  18384  nmhmcn  18617  aalioulem5  19732  xrlimcnp  20279  dmdmd  22896  mdsl0  22906  mdsl1i  22917  lmxrge0  23390  ghomf1olem  24016  ax13dfeq  24226  ispridlc  26798  infrglb  27825  bnj517  29233  equveliNEW7  29503  a12lem1  29752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator