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  2427  ax9ALT  2731  rspcimdv  3596  peano5  7894  isf34lem6  10399  inar1  10794  supsrlem  11130  r19.29uz  15374  o1of2  15634  o1rlimmul  15640  caucvg  15700  isprm5  16731  mrissmrid  17658  kgen2ss  23498  txlm  23591  isr0  23680  metcnpi3  24490  addcnlem  24809  nmhmcn  25076  aalioulem5  26301  xrlimcnp  26935  dmdmd  32286  mdsl0  32296  mdsl1i  32307  fldextrspunlsplem  33719  lmxrge0  33988  bnj517  34921  ax8dfeq  35821  in-ax8  36247  ss-ax8  36248  poimirlem29  37678  heicant  37684  ispridlc  38099  dffltz  42624  intabssd  43510  ss2iundf  43650  ismnushort  44292