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  912  nfimd  1896  axc15  2426  ax9ALT  2731  rspcimdv  3554  peano5  7844  isf34lem6  10302  inar1  10698  supsrlem  11034  r19.29uz  15313  o1of2  15575  o1rlimmul  15581  caucvg  15641  isprm5  16677  mrissmrid  17607  kgen2ss  23520  txlm  23613  isr0  23702  metcnpi3  24511  addcnlem  24830  nmhmcn  25087  aalioulem5  26302  xrlimcnp  26932  dmdmd  32371  mdsl0  32381  mdsl1i  32392  fldextrspunlsplem  33817  lmxrge0  34096  bnj517  35027  ax8dfeq  35978  in-ax8  36406  ss-ax8  36407  wl-dfcleq  37830  poimirlem29  37970  heicant  37976  ispridlc  38391  dffltz  43067  intabssd  43946  ss2iundf  44086  ismnushort  44728