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  912  nfimd  1894  axc15  2427  ax9ALT  2732  rspcimdv  3612  peano5  7915  isf34lem6  10420  inar1  10815  supsrlem  11151  r19.29uz  15389  o1of2  15649  o1rlimmul  15655  caucvg  15715  isprm5  16744  mrissmrid  17684  kgen2ss  23563  txlm  23656  isr0  23745  metcnpi3  24559  addcnlem  24886  nmhmcn  25153  aalioulem5  26378  xrlimcnp  27011  dmdmd  32319  mdsl0  32329  mdsl1i  32340  fldextrspunlsplem  33723  lmxrge0  33951  bnj517  34899  ax8dfeq  35799  in-ax8  36225  ss-ax8  36226  poimirlem29  37656  heicant  37662  ispridlc  38077  dffltz  42644  intabssd  43532  ss2iundf  43672  ismnushort  44320