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  4279  wefrc  5617  f1oweALT  7914  tfrlem9  8314  tz7.49  8374  oaordex  8483  dfac2b  10044  zorn2lem4  10412  zorn2lem7  10415  psslinpr  10944  facwordi  14215  ndvdssub  16339  pmtrfrn  19356  elcls  22977  elcls3  22987  neibl  24406  met2ndc  24428  itgcn  25763  branmfn  32068  atcvatlem  32348  atcvat4i  32360  umgr2cycllem  35132  satfv0fun  35363  prtlem15  38873  cvlsupr4  39343  cvlsupr5  39344  cvlsupr6  39345  2llnneN  39408  cvrat4  39442  llnexchb2  39868  cdleme48gfv1  40535  cdlemg6e  40621  dihord6apre  41255  dihord5b  41258  dihord5apre  41261  dihglblem5apreN  41290  dihglbcpreN  41299