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  rspcimdv  3341  peano5  7131  isf34lem6  9240  inar1  9635  supsrlem  9970  r19.29uz  14134  o1of2  14387  o1rlimmul  14393  caucvg  14453  isprm5  15466  mrissmrid  16348  kgen2ss  21406  txlm  21499  isr0  21588  metcnpi3  22398  addcnlem  22714  nmhmcn  22966  aalioulem5  24136  xrlimcnp  24740  dmdmd  29287  mdsl0  29297  mdsl1i  29308  lmxrge0  30126  bnj517  31081  ax8dfeq  31828  bj-mo3OLD  32957  bj-ax9-2  33016  poimirlem29  33568  heicant  33574  ispridlc  33999  intabssd  38233  ss2iundf  38268