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  922  nfimd  1913  axc15  2452  ax9ALT  2756  rspcimdv  3571  peano5  7870  isf34lem6  10334  inar1  10730  supsrlem  11066  r19.29uz  15361  o1of2  15623  o1rlimmul  15629  caucvg  15689  isprm5  16725  mrissmrid  17656  kgen2ss  23595  txlm  23688  isr0  23777  metcnpi3  24586  addcnlem  24905  nmhmcn  25162  aalioulem5  26377  xrlimcnp  27010  dmdmd  32449  mdsl0  32459  mdsl1i  32470  fldextrspunlsplem  33931  lmxrge0  34210  bnj517  35144  axpowg2  35407  axpowg3  35408  ax8dfeq  36110  in-ax8  36548  ss-ax8  36549  wl-dfcleq  37972  poimirlem29  38112  heicant  38118  ispridlc  38533  dffltz  43180  intabssd  44059  ss2iundf  44199  ismnushort  44841