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  4287  wefrc  5653  f1oweALT  7965  tfrlem9  8368  tz7.49  8428  oaordex  8539  dfac2b  10110  zorn2lem4  10479  zorn2lem7  10482  psslinpr  11012  facwordi  14321  ndvdssub  16463  pmtrfrn  19524  elcls  23195  elcls3  23205  neibl  24623  met2ndc  24645  itgcn  25969  branmfn  32394  atcvatlem  32674  atcvat4i  32686  umgr2cycllem  35527  satfv0fun  35758  prtlem15  39534  cvlsupr4  40004  cvlsupr5  40005  cvlsupr6  40006  2llnneN  40068  cvrat4  40102  llnexchb2  40528  cdleme48gfv1  41195  cdlemg6e  41281  dihord6apre  41915  dihord5b  41918  dihord5apre  41921  dihglblem5apreN  41950  dihglbcpreN  41959