Theorem ad5ant14 757

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 715	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	ad4ant13 751	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:  leexp1a  14082  cpmatinvcl  22633  restcld  23088  ustuqtop3  24159  legval  28563  ccatws1f1o  32930  mplvrpmrhm  33575  lssdimle  33618  zarcls1  33880  lindsenlbs  37661  matunitlindflem1  37662  modelaxrep  45020  xrralrecnnle  45427  limclner  45695  limsupub2  45856  xlimliminflimsup  45906  pimdecfgtioo  46761  pimincfltioo  46762