Theorem imp4a 423

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 422	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	ex 413	1 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  imp4d  425  imp55  443  imp511  444  reuss2  4314  wefrc  5669  f1oweALT  7955  tfrlem9  8381  tz7.49  8441  oaordex  8554  dfac2b  10121  zorn2lem4  10490  zorn2lem7  10493  psslinpr  11022  facwordi  14245  ndvdssub  16348  pmtrfrn  19320  elcls  22568  elcls3  22578  neibl  24001  met2ndc  24023  itgcn  25353  branmfn  31345  atcvatlem  31625  atcvat4i  31637  umgr2cycllem  34119  satfv0fun  34350  prtlem15  37733  cvlsupr4  38203  cvlsupr5  38204  cvlsupr6  38205  2llnneN  38268  cvrat4  38302  llnexchb2  38728  cdleme48gfv1  39395  cdlemg6e  39481  dihord6apre  40115  dihord5b  40118  dihord5apre  40121  dihglblem5apreN  40150  dihglbcpreN  40159