Theorem imp4a 422

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.)

Hypothesis

Ref	Expression
imp4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
imp4a	⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))

Proof of Theorem imp4a

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	imp4b 421	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	ex 412	1 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  imp4d  424  imp55  442  imp511  443  reuss2  4326  wefrc  5679  f1oweALT  7997  tfrlem9  8425  tz7.49  8485  oaordex  8596  dfac2b  10171  zorn2lem4  10539  zorn2lem7  10542  psslinpr  11071  facwordi  14328  ndvdssub  16446  pmtrfrn  19476  elcls  23081  elcls3  23091  neibl  24514  met2ndc  24536  itgcn  25880  branmfn  32124  atcvatlem  32404  atcvat4i  32416  umgr2cycllem  35145  satfv0fun  35376  prtlem15  38876  cvlsupr4  39346  cvlsupr5  39347  cvlsupr6  39348  2llnneN  39411  cvrat4  39445  llnexchb2  39871  cdleme48gfv1  40538  cdlemg6e  40624  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dihglblem5apreN  41293  dihglbcpreN  41302