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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1d  83  orim12dALT  925  nfimd  1927  axc15  2451  ax9ALT  2755  rspcimdv  3566  peano5  7890  isf34lem6  10382  inar1  10784  supsrlem  11120  r19.29uz  15438  o1of2  15700  o1rlimmul  15706  caucvg  15766  isprm5  16798  mrissmrid  17729  kgen2ss  23781  txlm  23874  isr0  23963  metcnpi3  24772  addcnlem  25091  nmhmcn  25348  aalioulem5  26572  xrlimcnp  27205  dmdmd  32781  mdsl0  32791  mdsl1i  32802  fldextrspunlsplem  34183  lmxrge0  34462  bnj517  35394  axpowg2  35673  axpowg3  35674  ax8dfeq  36375  in-ax8  36844  ss-ax8  36845  wl-dfcleq  38268  poimirlem29  38398  heicant  38404  ispridlc  38820  dffltz  43480  intabssd  44359  ss2iundf  44499  ismnushort  45125