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  2452  ax9ALT  2756  rspcimdv  3567  peano5  7903  isf34lem6  10451  inar1  10853  supsrlem  11189  r19.29uz  15511  o1of2  15773  o1rlimmul  15779  caucvg  15839  isprm5  16876  mrissmrid  17808  kgen2ss  23867  txlm  23960  isr0  24049  metcnpi3  24858  addcnlem  25177  nmhmcn  25434  aalioulem5  26656  xrlimcnp  27289  dmdmd  32895  mdsl0  32905  mdsl1i  32916  fldextrspunlsplem  34298  lmxrge0  34577  bnj517  35508  axpowg2  35798  axpowg3  35799  ax8dfeq  36540  in-ax8  36993  ss-ax8  36994  wl-dfcleq  38417  poimirlem29  38547  heicant  38553  ispridlc  38984  dffltz  43650  intabssd  44504  ss2iundf  44644  ismnushort  45270