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  7905  isf34lem6  10459  inar1  10861  supsrlem  11197  r19.29uz  15519  o1of2  15781  o1rlimmul  15787  caucvg  15847  isprm5  16884  mrissmrid  17816  kgen2ss  23875  txlm  23968  isr0  24057  metcnpi3  24866  addcnlem  25185  nmhmcn  25442  aalioulem5  26664  xrlimcnp  27297  dmdmd  32903  mdsl0  32913  mdsl1i  32924  fldextrspunlsplem  34348  lmxrge0  34627  bnj517  35558  axpowg2  35864  axpowg3  35865  ax8dfeq  36635  in-ax8  37088  ss-ax8  37089  wl-dfcleq  38513  poimirlem29  38643  heicant  38649  ispridlc  39080  dffltz  43746  intabssd  44596  ss2iundf  44735  ismnushort  45361