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  909  nfimd  1895  axc15  2433  ax9ALT  2794  rspcimdv  3561  peano5  7585  isf34lem6  9791  inar1  10186  supsrlem  10522  r19.29uz  14702  o1of2  14961  o1rlimmul  14967  caucvg  15027  isprm5  16041  mrissmrid  16904  kgen2ss  22160  txlm  22253  isr0  22342  metcnpi3  23153  addcnlem  23469  nmhmcn  23725  aalioulem5  24932  xrlimcnp  25554  dmdmd  30083  mdsl0  30093  mdsl1i  30104  lmxrge0  31305  bnj517  32267  ax8dfeq  33156  poimirlem29  35086  heicant  35092  ispridlc  35508  dffltz  39615  intabssd  40227  ss2iundf  40360