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  4267  wefrc  5618  f1oweALT  7918  tfrlem9  8317  tz7.49  8377  oaordex  8486  dfac2b  10044  zorn2lem4  10412  zorn2lem7  10415  psslinpr  10945  facwordi  14242  ndvdssub  16369  pmtrfrn  19424  elcls  23048  elcls3  23058  neibl  24476  met2ndc  24498  itgcn  25822  branmfn  32191  atcvatlem  32471  atcvat4i  32483  umgr2cycllem  35338  satfv0fun  35569  prtlem15  39335  cvlsupr4  39805  cvlsupr5  39806  cvlsupr6  39807  2llnneN  39869  cvrat4  39903  llnexchb2  40329  cdleme48gfv1  40996  cdlemg6e  41082  dihord6apre  41716  dihord5b  41719  dihord5apre  41722  dihglblem5apreN  41751  dihglbcpreN  41760