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  907  nfimd  1888  axc15  2440  ax9ALT  2821  rspcimdv  3616  peano5  7596  isf34lem6  9794  inar1  10189  supsrlem  10525  r19.29uz  14703  o1of2  14962  o1rlimmul  14968  caucvg  15028  isprm5  16043  mrissmrid  16904  kgen2ss  22081  txlm  22174  isr0  22263  metcnpi3  23073  addcnlem  23389  nmhmcn  23641  aalioulem5  24842  xrlimcnp  25462  dmdmd  29993  mdsl0  30003  mdsl1i  30014  lmxrge0  31083  bnj517  32045  ax8dfeq  32929  poimirlem29  34790  heicant  34796  ispridlc  35218  dffltz  39138  intabssd  39752  ss2iundf  39871
  Copyright terms: Public domain W3C validator