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  911  nfimd  1892  axc15  2425  ax9ALT  2730  rspcimdv  3612  peano5  7916  isf34lem6  10418  inar1  10813  supsrlem  11149  r19.29uz  15386  o1of2  15646  o1rlimmul  15652  caucvg  15712  isprm5  16741  mrissmrid  17686  kgen2ss  23579  txlm  23672  isr0  23761  metcnpi3  24575  addcnlem  24900  nmhmcn  25167  aalioulem5  26393  xrlimcnp  27026  dmdmd  32329  mdsl0  32339  mdsl1i  32350  lmxrge0  33913  bnj517  34878  ax8dfeq  35780  in-ax8  36207  ss-ax8  36208  poimirlem29  37636  heicant  37642  ispridlc  38057  dffltz  42621  intabssd  43509  ss2iundf  43649  ismnushort  44297