Theorem imim12d 82

Description: Deduction combining antecedents and consequents. Deduction associated with imim12 106 and imim12i 63. (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

Step	Hyp	Ref	Expression
1		imim12d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imim12d.2	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
3	2	imim2d 58	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜒 → 𝜏)))
4	1, 3	syl5d 74	1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜏)))

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  83  orim12dALT  924  nfimd  1924  axc15  2454  ax9ALT  2758  rspcimdv  3572  peano5  7891  isf34lem6  10365  inar1  10761  supsrlem  11097  r19.29uz  15404  o1of2  15666  o1rlimmul  15672  caucvg  15732  isprm5  16767  mrissmrid  17698  kgen2ss  23693  txlm  23786  isr0  23875  metcnpi3  24684  addcnlem  25003  nmhmcn  25260  aalioulem5  26480  xrlimcnp  27114  dmdmd  32633  mdsl0  32643  mdsl1i  32654  fldextrspunlsplem  34044  lmxrge0  34323  bnj517  35254  axpowg2  35541  axpowg3  35542  ax8dfeq  36269  in-ax8  36717  ss-ax8  36718  wl-dfcleq  38141  poimirlem29  38281  heicant  38287  ispridlc  38702  dffltz  43349  intabssd  44228  ss2iundf  44368  ismnushort  44994