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  1895  axc15  2426  ax9ALT  2731  rspcimdv  3566  peano5  7835  isf34lem6  10290  inar1  10686  supsrlem  11022  r19.29uz  15274  o1of2  15536  o1rlimmul  15542  caucvg  15602  isprm5  16634  mrissmrid  17564  kgen2ss  23499  txlm  23592  isr0  23681  metcnpi3  24490  addcnlem  24809  nmhmcn  25076  aalioulem5  26300  xrlimcnp  26934  dmdmd  32375  mdsl0  32385  mdsl1i  32396  fldextrspunlsplem  33830  lmxrge0  34109  bnj517  35041  ax8dfeq  35990  in-ax8  36418  ss-ax8  36419  poimirlem29  37846  heicant  37852  ispridlc  38267  dffltz  42873  intabssd  43756  ss2iundf  43896  ismnushort  44538