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  15392  o1of2  15654  o1rlimmul  15660  caucvg  15720  isprm5  16756  mrissmrid  17687  kgen2ss  23673  txlm  23766  isr0  23855  metcnpi3  24664  addcnlem  24983  nmhmcn  25240  aalioulem5  26458  xrlimcnp  27091  dmdmd  32561  mdsl0  32571  mdsl1i  32582  fldextrspunlsplem  33980  lmxrge0  34259  bnj517  35190  axpowg2  35455  axpowg3  35456  ax8dfeq  36159  in-ax8  36597  ss-ax8  36598  wl-dfcleq  38020  poimirlem29  38160  heicant  38166  ispridlc  38581  dffltz  43228  intabssd  44107  ss2iundf  44247  ismnushort  44875