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  4289  wefrc  5632  f1oweALT  7951  tfrlem9  8353  tz7.49  8413  oaordex  8522  dfac2b  10084  zorn2lem4  10452  zorn2lem7  10455  psslinpr  10984  facwordi  14254  ndvdssub  16379  pmtrfrn  19388  elcls  22960  elcls3  22970  neibl  24389  met2ndc  24411  itgcn  25746  branmfn  32034  atcvatlem  32314  atcvat4i  32326  umgr2cycllem  35127  satfv0fun  35358  prtlem15  38868  cvlsupr4  39338  cvlsupr5  39339  cvlsupr6  39340  2llnneN  39403  cvrat4  39437  llnexchb2  39863  cdleme48gfv1  40530  cdlemg6e  40616  dihord6apre  41250  dihord5b  41253  dihord5apre  41256  dihglblem5apreN  41285  dihglbcpreN  41294