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  917  nfimd  1901  axc15  2430  ax9ALT  2734  rspcimdv  3550  peano5  7833  isf34lem6  10293  inar1  10689  supsrlem  11025  r19.29uz  15304  o1of2  15566  o1rlimmul  15572  caucvg  15632  isprm5  16668  mrissmrid  17598  kgen2ss  23538  txlm  23631  isr0  23720  metcnpi3  24529  addcnlem  24848  nmhmcn  25105  aalioulem5  26320  xrlimcnp  26950  dmdmd  32389  mdsl0  32399  mdsl1i  32410  fldextrspunlsplem  33857  lmxrge0  34136  bnj517  35067  axpowg2  35328  axpowg3  35329  ax8dfeq  36024  in-ax8  36452  ss-ax8  36453  wl-dfcleq  37876  poimirlem29  38016  heicant  38022  ispridlc  38437  dffltz  43084  intabssd  43963  ss2iundf  44103  ismnushort  44745