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  2321  moOLD  2327  rspcimdv  3215  peano5  6701  isf34lem6  8756  inar1  9149  supsrlem  9484  uzindOLD  10951  r19.29uz  13142  o1of2  13394  o1rlimmul  13400  caucvg  13460  isprm5  14108  mrissmrid  14892  kgen2ss  19791  txlm  19884  isr0  19973  metcnpi3  20784  addcnlem  21103  nmhmcn  21338  aalioulem5  22466  xrlimcnp  23026  dmdmd  26895  mdsl0  26905  mdsl1i  26916  xrge0infss  27248  lmxrge0  27570  ghomf1olem  28509  ax8dfeq  28808  heicant  29626  ispridlc  30070  infrglb  31140  bnj517  33022
  Copyright terms: Public domain W3C validator