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 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1d  83  orim12dALT  925  nfimd  1927  axc15  2457  ax9ALT  2761  rspcimdv  3574  peano5  7899  isf34lem6  10382  inar1  10778  supsrlem  11114  r19.29uz  15428  o1of2  15690  o1rlimmul  15696  caucvg  15756  isprm5  16791  mrissmrid  17722  kgen2ss  23749  txlm  23842  isr0  23931  metcnpi3  24740  addcnlem  25059  nmhmcn  25316  aalioulem5  26536  xrlimcnp  27170  dmdmd  32689  mdsl0  32699  mdsl1i  32710  fldextrspunlsplem  34094  lmxrge0  34373  bnj517  35305  axpowg2  35584  axpowg3  35585  ax8dfeq  36309  in-ax8  36777  ss-ax8  36778  wl-dfcleq  38201  poimirlem29  38341  heicant  38347  ispridlc  38762  dffltz  43407  intabssd  44286  ss2iundf  44426  ismnushort  45052