MPE Home 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  orim12dALT  910  nfimd  1897  axc15  2421  ax9ALT  2727  rspcimdv  3602  peano5  7886  peano5OLD  7887  isf34lem6  10377  inar1  10772  supsrlem  11108  r19.29uz  15301  o1of2  15561  o1rlimmul  15567  caucvg  15629  isprm5  16648  mrissmrid  17589  kgen2ss  23279  txlm  23372  isr0  23461  metcnpi3  24275  addcnlem  24600  nmhmcn  24860  aalioulem5  26073  xrlimcnp  26697  dmdmd  31808  mdsl0  31818  mdsl1i  31829  lmxrge0  33218  bnj517  34182  ax8dfeq  35062  poimirlem29  36820  heicant  36826  ispridlc  37241  dffltz  41678  intabssd  42572  ss2iundf  42712  ismnushort  43362
  Copyright terms: Public domain W3C validator