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

Theorem imim12d 79
 Description: Deduction combining antecedents and consequents. Deduction associated with imim12 103 and imim12i 60. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mel L. O'Cat, 30-Oct-2011.)
Hypotheses
Ref Expression
imim12d.1 (𝜑 → (𝜓𝜒))
imim12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
imim12d (𝜑 → ((𝜒𝜃) → (𝜓𝜏)))

Proof of Theorem imim12d
StepHypRef Expression
1 imim12d.1 . 2 (𝜑 → (𝜓𝜒))
2 imim12d.2 . . 3 (𝜑 → (𝜃𝜏))
32imim2d 55 . 2 (𝜑 → ((𝜒𝜃) → (𝜒𝜏)))
41, 3syl5d 71 1 (𝜑 → ((𝜒𝜃) → (𝜓𝜏)))
 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  80  rspcimdv  3283  peano5  6981  isf34lem6  9085  inar1  9476  supsrlem  9811  r19.29uz  13938  o1of2  14191  o1rlimmul  14197  caucvg  14257  isprm5  15257  mrissmrid  16124  kgen2ss  21168  txlm  21261  isr0  21350  metcnpi3  22161  addcnlem  22475  nmhmcn  22728  aalioulem5  23895  xrlimcnp  24495  dmdmd  28543  mdsl0  28553  mdsl1i  28564  lmxrge0  29326  bnj517  30209  ax8dfeq  30948  bj-mo3OLD  32022  poimirlem29  32608  heicant  32614  ispridlc  33039  intabssd  36935  ss2iundf  36970
 Copyright terms: Public domain W3C validator