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  912  nfimd  1894  axc15  2427  ax9ALT  2732  rspcimdv  3612  peano5  7915  isf34lem6  10420  inar1  10815  supsrlem  11151  r19.29uz  15389  o1of2  15649  o1rlimmul  15655  caucvg  15715  isprm5  16744  mrissmrid  17684  kgen2ss  23563  txlm  23656  isr0  23745  metcnpi3  24559  addcnlem  24886  nmhmcn  25153  aalioulem5  26378  xrlimcnp  27011  dmdmd  32319  mdsl0  32329  mdsl1i  32340  fldextrspunlsplem  33723  lmxrge0  33951  bnj517  34899  ax8dfeq  35799  in-ax8  36225  ss-ax8  36226  poimirlem29  37656  heicant  37662  ispridlc  38077  dffltz  42644  intabssd  43532  ss2iundf  43672  ismnushort  44320
  Copyright terms: Public domain W3C validator