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

Theorem imim12d 76
Description: Deduction combining antecedents and consequents. Deduction associated with imim12 99 and imim12i 58. (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 53 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ch  ->  ta ) ) )
41, 3syl5d 68 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  77  rspcimdv  3137  peano5  6735  isf34lem6  8828  inar1  9218  supsrlem  9553  r19.29uz  13490  o1of2  13753  o1rlimmul  13759  caucvg  13822  isprm5  14730  mrissmrid  15625  kgen2ss  20647  txlm  20740  isr0  20829  metcnpi3  21639  addcnlem  21974  nmhmcn  22212  aalioulem5  23371  xrlimcnp  23973  dmdmd  28034  mdsl0  28044  mdsl1i  28055  xrge0infssOLD  28416  lmxrge0  28832  bnj517  29768  ghomf1olem  30384  ax8dfeq  30516  bj-mo3OLD  31515  poimirlem29  32033  heicant  32039  ispridlc  32367  intabssd  36287  ss2iundf  36322  infrglbOLD  37766
  Copyright terms: Public domain W3C validator