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

Theorem imim12d 81
 Description: Deduction combining antecedents and consequents. Deduction associated with imim12 105 and imim12i 62. (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 57 . 2 (𝜑 → ((𝜒𝜃) → (𝜒𝜏)))
41, 3syl5d 73 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  82  rspcimdv  3341  peano5  7131  isf34lem6  9240  inar1  9635  supsrlem  9970  r19.29uz  14134  o1of2  14387  o1rlimmul  14393  caucvg  14453  isprm5  15466  mrissmrid  16348  kgen2ss  21406  txlm  21499  isr0  21588  metcnpi3  22398  addcnlem  22714  nmhmcn  22966  aalioulem5  24136  xrlimcnp  24740  dmdmd  29287  mdsl0  29297  mdsl1i  29308  lmxrge0  30126  bnj517  31081  ax8dfeq  31828  bj-mo3OLD  32957  bj-ax9-2  33016  poimirlem29  33568  heicant  33574  ispridlc  33999  intabssd  38233  ss2iundf  38268
 Copyright terms: Public domain W3C validator