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  908  nfimd  1898  axc15  2422  ax9ALT  2733  rspcimdv  3541  peano5  7714  peano5OLD  7715  isf34lem6  10067  inar1  10462  supsrlem  10798  r19.29uz  14990  o1of2  15250  o1rlimmul  15256  caucvg  15318  isprm5  16340  mrissmrid  17267  kgen2ss  22614  txlm  22707  isr0  22796  metcnpi3  23608  addcnlem  23933  nmhmcn  24189  aalioulem5  25401  xrlimcnp  26023  dmdmd  30563  mdsl0  30573  mdsl1i  30584  lmxrge0  31804  bnj517  32765  ax8dfeq  33680  poimirlem29  35733  heicant  35739  ispridlc  36155  dffltz  40387  intabssd  41024  ss2iundf  41156  ismnushort  41808