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  936  nfimd  1993  rspcimdv  3497  peano5  7322  isf34lem6  9489  inar1  9884  supsrlem  10219  r19.29uz  14428  o1of2  14681  o1rlimmul  14687  caucvg  14747  isprm5  15749  mrissmrid  16613  kgen2ss  21684  txlm  21777  isr0  21866  metcnpi3  22676  addcnlem  22992  nmhmcn  23244  aalioulem5  24429  xrlimcnp  25044  dmdmd  29677  mdsl0  29687  mdsl1i  29698  lmxrge0  30507  bnj517  31465  ax8dfeq  32209  bj-mo3OLD  33320  bj-ax9-2  33375  poimirlem29  33920  heicant  33926  ispridlc  34349  intabssd  38688  ss2iundf  38723