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  4292  wefrc  5635  f1oweALT  7954  tfrlem9  8356  tz7.49  8416  oaordex  8525  dfac2b  10091  zorn2lem4  10459  zorn2lem7  10462  psslinpr  10991  facwordi  14261  ndvdssub  16386  pmtrfrn  19395  elcls  22967  elcls3  22977  neibl  24396  met2ndc  24418  itgcn  25753  branmfn  32041  atcvatlem  32321  atcvat4i  32333  umgr2cycllem  35134  satfv0fun  35365  prtlem15  38875  cvlsupr4  39345  cvlsupr5  39346  cvlsupr6  39347  2llnneN  39410  cvrat4  39444  llnexchb2  39870  cdleme48gfv1  40537  cdlemg6e  40623  dihord6apre  41257  dihord5b  41260  dihord5apre  41263  dihglblem5apreN  41292  dihglbcpreN  41301