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  1894  axc15  2420  ax9ALT  2724  rspcimdv  3569  peano5  7833  isf34lem6  10293  inar1  10688  supsrlem  11024  r19.29uz  15276  o1of2  15538  o1rlimmul  15544  caucvg  15604  isprm5  16636  mrissmrid  17565  kgen2ss  23458  txlm  23551  isr0  23640  metcnpi3  24450  addcnlem  24769  nmhmcn  25036  aalioulem5  26260  xrlimcnp  26894  dmdmd  32262  mdsl0  32272  mdsl1i  32283  fldextrspunlsplem  33644  lmxrge0  33918  bnj517  34851  ax8dfeq  35771  in-ax8  36197  ss-ax8  36198  poimirlem29  37628  heicant  37634  ispridlc  38049  dffltz  42607  intabssd  43492  ss2iundf  43632  ismnushort  44274