Theorem imim12d 81

Description: Deduction combining antecedents and consequents. Deduction associated with imim12 105 and imim12i 62. (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 57	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜒 → 𝜏)))
4	1, 3	syl5d 73	1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜏)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imim1d  82  orim12dALT  911  nfimd  1894  axc15  2421  ax9ALT  2725  rspcimdv  3581  peano5  7872  isf34lem6  10340  inar1  10735  supsrlem  11071  r19.29uz  15324  o1of2  15586  o1rlimmul  15592  caucvg  15652  isprm5  16684  mrissmrid  17609  kgen2ss  23449  txlm  23542  isr0  23631  metcnpi3  24441  addcnlem  24760  nmhmcn  25027  aalioulem5  26251  xrlimcnp  26885  dmdmd  32236  mdsl0  32246  mdsl1i  32257  fldextrspunlsplem  33675  lmxrge0  33949  bnj517  34882  ax8dfeq  35793  in-ax8  36219  ss-ax8  36220  poimirlem29  37650  heicant  37656  ispridlc  38071  dffltz  42629  intabssd  43515  ss2iundf  43655  ismnushort  44297