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

Theorem imim12d 70
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 50 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ch  ->  ta ) ) )
41, 3syl5d 64 1  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1d  71  equveliOLD  2086  mo  2303  rspcimdv  3053  peano5  4868  tfrlem1  6636  isf34lem6  8260  inar1  8650  supsrlem  8986  uzindOLD  10364  r19.29uz  12154  o1of2  12406  o1rlimmul  12412  caucvg  12472  isprm5  13112  mrissmrid  13866  kgen2ss  17587  txlm  17680  isr0  17769  metcnpi3  18576  addcnlem  18894  nmhmcn  19128  aalioulem5  20253  xrlimcnp  20807  dmdmd  23803  mdsl0  23813  mdsl1i  23824  lmxrge0  24337  ghomf1olem  25105  ax13dfeq  25426  ispridlc  26680  infrglb  27698  bnj517  29256  equveliNEW7  29528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator