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

Theorem imim12d 77
Description: Deduction combining antecedents and consequents. Deduction associated with imim12 100 and imim12i 59. (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 54 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ch  ->  ta ) ) )
41, 3syl5d 69 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  78  rspcimdv  3151  peano5  6716  isf34lem6  8810  inar1  9200  supsrlem  9535  r19.29uz  13413  o1of2  13676  o1rlimmul  13682  caucvg  13745  isprm5  14651  mrissmrid  15547  kgen2ss  20570  txlm  20663  isr0  20752  metcnpi3  21561  addcnlem  21896  nmhmcn  22134  aalioulem5  23292  xrlimcnp  23894  dmdmd  27953  mdsl0  27963  mdsl1i  27974  xrge0infssOLD  28341  lmxrge0  28758  bnj517  29696  ghomf1olem  30312  ax8dfeq  30445  bj-mo3OLD  31447  poimirlem29  31969  heicant  31975  ispridlc  32303  intabssd  36216  ss2iundf  36251  infrglbOLD  37669
  Copyright terms: Public domain W3C validator