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  14322  lindsenlbs  22163  matunitlindflem1  23000  cpmatinvcl  23041  restcld  23496  ustuqtop3  24568  legval  29053  ccatws1f1o  33561  mplvrpmrhm  34226  esplyfval1  34252  lssdimle  34287  zarcls1  34548  modelaxrep  46065  xrralrecnnle  46488  limclner  46755  limsupub2  46916  xlimliminflimsup  46966  pimdecfgtioo  47821  pimincfltioo  47822