Theorem imp4a 427

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imp4d  429  imp55  447  imp511  448  reuss2  4279  wefrc  5655  f1oweALT  7965  tfrlem9  8368  tz7.49  8428  oaordex  8539  dfac2b  10110  zorn2lem4  10478  zorn2lem7  10481  psslinpr  11011  facwordi  14321  ndvdssub  16462  pmtrfrn  19523  elcls  23230  elcls3  23240  neibl  24658  met2ndc  24680  itgcn  26004  branmfn  32457  atcvatlem  32737  atcvat4i  32749  umgr2cycllem  35632  satfv0fun  35863  prtlem15  39649  cvlsupr4  40119  cvlsupr5  40120  cvlsupr6  40121  2llnneN  40183  cvrat4  40217  llnexchb2  40643  cdleme48gfv1  41310  cdlemg6e  41396  dihord6apre  42030  dihord5b  42033  dihord5apre  42036  dihglblem5apreN  42065  dihglbcpreN  42074