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 52 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ch  ->  ta ) ) )
41, 3syl5d 67 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  2306  moOLD  2312  rspcimdv  3173  peano5  6602  isf34lem6  8653  inar1  9046  supsrlem  9382  uzindOLD  10840  r19.29uz  12949  o1of2  13201  o1rlimmul  13207  caucvg  13267  isprm5  13909  mrissmrid  14690  kgen2ss  19253  txlm  19346  isr0  19435  metcnpi3  20246  addcnlem  20565  nmhmcn  20800  aalioulem5  21928  xrlimcnp  22488  dmdmd  25849  mdsl0  25859  mdsl1i  25870  xrge0infss  26197  lmxrge0  26520  ghomf1olem  27450  ax8dfeq  27749  heicant  28567  ispridlc  29011  infrglb  29912  bnj517  32181
  Copyright terms: Public domain W3C validator