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  1929  axc15  2454  ax9ALT  2758  rspcimdv  3570  peano5  7939  isf34lem6  10497  inar1  10899  supsrlem  11235  r19.29uz  15562  o1of2  15824  o1rlimmul  15830  caucvg  15890  isprm5  16927  mrissmrid  17865  kgen2ss  23929  txlm  24022  isr0  24111  metcnpi3  24920  addcnlem  25239  nmhmcn  25496  aalioulem5  26720  xrlimcnp  27353  dmdmd  32959  mdsl0  32969  mdsl1i  32980  fldextrspunlsplem  34416  lmxrge0  34695  bnj517  35626  axpowg2  35956  axpowg3  35957  ax8dfeq  36775  in-ax8  37228  ss-ax8  37229  wl-dfcleq  38705  poimirlem29  38835  heicant  38841  ispridlc  39270  dffltz  43936  intabssd  44781  ss2iundf  44920  ismnushort  45546