Theorem imim12d 79

Description: Deduction combining antecedents and consequents. Deduction associated with imim12 103 and imim12i 60. (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 55	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜒 → 𝜏)))
4	1, 3	syl5d 71	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  80  rspcimdv  3283  peano5  6981  isf34lem6  9085  inar1  9476  supsrlem  9811  r19.29uz  13938  o1of2  14191  o1rlimmul  14197  caucvg  14257  isprm5  15257  mrissmrid  16124  kgen2ss  21168  txlm  21261  isr0  21350  metcnpi3  22161  addcnlem  22475  nmhmcn  22728  aalioulem5  23895  xrlimcnp  24495  dmdmd  28543  mdsl0  28553  mdsl1i  28564  lmxrge0  29326  bnj517  30209  ax8dfeq  30948  bj-mo3OLD  32022  poimirlem29  32608  heicant  32614  ispridlc  33039  intabssd  36935  ss2iundf  36970