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  1926  axc15  2451  ax9ALT  2755  rspcimdv  3566  peano5  7906  isf34lem6  10462  inar1  10864  supsrlem  11200  r19.29uz  15524  o1of2  15786  o1rlimmul  15792  caucvg  15852  isprm5  16889  mrissmrid  17821  kgen2ss  23880  txlm  23973  isr0  24062  metcnpi3  24871  addcnlem  25190  nmhmcn  25447  aalioulem5  26669  xrlimcnp  27302  dmdmd  32908  mdsl0  32918  mdsl1i  32929  fldextrspunlsplem  34352  lmxrge0  34631  bnj517  35562  axpowg2  35872  axpowg3  35873  ax8dfeq  36653  in-ax8  37106  ss-ax8  37107  wl-dfcleq  38531  poimirlem29  38661  heicant  38667  ispridlc  39098  dffltz  43764  intabssd  44614  ss2iundf  44753  ismnushort  45379