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  1896  axc15  2427  ax9ALT  2732  rspcimdv  3555  peano5  7837  isf34lem6  10293  inar1  10689  supsrlem  11025  r19.29uz  15304  o1of2  15566  o1rlimmul  15572  caucvg  15632  isprm5  16668  mrissmrid  17598  kgen2ss  23530  txlm  23623  isr0  23712  metcnpi3  24521  addcnlem  24840  nmhmcn  25097  aalioulem5  26313  xrlimcnp  26945  dmdmd  32386  mdsl0  32396  mdsl1i  32407  fldextrspunlsplem  33833  lmxrge0  34112  bnj517  35043  ax8dfeq  35994  in-ax8  36422  ss-ax8  36423  wl-dfcleq  37844  poimirlem29  37984  heicant  37990  ispridlc  38405  dffltz  43081  intabssd  43964  ss2iundf  44104  ismnushort  44746