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  4278  wefrc  5618  f1oweALT  7916  tfrlem9  8316  tz7.49  8376  oaordex  8485  dfac2b  10041  zorn2lem4  10409  zorn2lem7  10412  psslinpr  10942  facwordi  14212  ndvdssub  16336  pmtrfrn  19387  elcls  23017  elcls3  23027  neibl  24445  met2ndc  24467  itgcn  25802  branmfn  32180  atcvatlem  32460  atcvat4i  32472  umgr2cycllem  35334  satfv0fun  35565  prtlem15  39135  cvlsupr4  39605  cvlsupr5  39606  cvlsupr6  39607  2llnneN  39669  cvrat4  39703  llnexchb2  40129  cdleme48gfv1  40796  cdlemg6e  40882  dihord6apre  41516  dihord5b  41519  dihord5apre  41522  dihglblem5apreN  41551  dihglbcpreN  41560