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  910  nfimd  1893  axc15  2430  ax9ALT  2735  rspcimdv  3625  peano5  7932  peano5OLD  7933  isf34lem6  10449  inar1  10844  supsrlem  11180  r19.29uz  15399  o1of2  15659  o1rlimmul  15665  caucvg  15727  isprm5  16754  mrissmrid  17699  kgen2ss  23584  txlm  23677  isr0  23766  metcnpi3  24580  addcnlem  24905  nmhmcn  25172  aalioulem5  26396  xrlimcnp  27029  dmdmd  32332  mdsl0  32342  mdsl1i  32353  lmxrge0  33898  bnj517  34861  ax8dfeq  35762  in-ax8  36190  ss-ax8  36191  poimirlem29  37609  heicant  37615  ispridlc  38030  dffltz  42589  intabssd  43481  ss2iundf  43621  ismnushort  44270