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

Theorem imim12d 74
Description: Deduction combining antecedents and consequents. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mel L. 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 51 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ch  ->  ta ) ) )
41, 3syl5d 66 1  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  ta ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1d  75  mo3OLD  2279  rspcimdv  3160  peano5  6706  isf34lem6  8791  inar1  9182  supsrlem  9517  r19.29uz  13330  o1of2  13582  o1rlimmul  13588  caucvg  13648  isprm5  14460  mrissmrid  15253  kgen2ss  20346  txlm  20439  isr0  20528  metcnpi3  21339  addcnlem  21658  nmhmcn  21893  aalioulem5  23022  xrlimcnp  23622  dmdmd  27618  mdsl0  27628  mdsl1i  27639  xrge0infss  28008  lmxrge0  28373  bnj517  29257  ghomf1olem  29873  ax8dfeq  30005  heicant  31401  ispridlc  31729  ss2iundf  35618  infrglb  36933
  Copyright terms: Public domain W3C validator