Theorem ad5ant14 770

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad5ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad5ant14	⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒)

Proof of Theorem ad5ant14

Step	Hyp	Ref	Expression
1		ad5ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 728	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	ad4ant13 764	1 ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  leexp1a  14243  lindsenlbs  22070  matunitlindflem1  22907  cpmatinvcl  22948  restcld  23403  ustuqtop3  24475  legval  28934  ccatws1f1o  33401  mplvrpmrhm  34065  esplyfval1  34091  lssdimle  34126  zarcls1  34387  modelaxrep  45812  xrralrecnnle  46220  limclner  46487  limsupub2  46648  xlimliminflimsup  46698  pimdecfgtioo  47553  pimincfltioo  47554