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 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜏)))

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  83  orim12dALT  924  nfimd  1917  axc15  2456  ax9ALT  2760  rspcimdv  3574  peano5  7878  isf34lem6  10352  inar1  10748  supsrlem  11084  r19.29uz  15390  o1of2  15652  o1rlimmul  15658  caucvg  15718  isprm5  16754  mrissmrid  17685  kgen2ss  23669  txlm  23762  isr0  23851  metcnpi3  24660  addcnlem  24979  nmhmcn  25236  aalioulem5  26454  xrlimcnp  27087  dmdmd  32557  mdsl0  32567  mdsl1i  32578  fldextrspunlsplem  33975  lmxrge0  34254  bnj517  35185  axpowg2  35450  axpowg3  35451  ax8dfeq  36154  in-ax8  36592  ss-ax8  36593  wl-dfcleq  38015  poimirlem29  38155  heicant  38161  ispridlc  38576  dffltz  43223  intabssd  44102  ss2iundf  44242  ismnushort  44870