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  1897  axc15  2422  ax9ALT  2733  rspcimdv  3550  peano5  7732  peano5OLD  7733  isf34lem6  10125  inar1  10520  supsrlem  10856  r19.29uz  15051  o1of2  15311  o1rlimmul  15317  caucvg  15379  isprm5  16401  mrissmrid  17339  kgen2ss  22695  txlm  22788  isr0  22877  metcnpi3  23691  addcnlem  24016  nmhmcn  24272  aalioulem5  25485  xrlimcnp  26107  dmdmd  30649  mdsl0  30659  mdsl1i  30670  lmxrge0  31889  bnj517  32852  ax8dfeq  33761  poimirlem29  35793  heicant  35799  ispridlc  36215  dffltz  40458  intabssd  41095  ss2iundf  41227  ismnushort  41879