Theorem ad5ant15 771

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
ad5ant15	⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒)

Proof of Theorem ad5ant15

Step	Hyp	Ref	Expression
1		ad5ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 728	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	ad4ant14 765	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:  summolem2  15806  ntrivcvg  15990  xkoccn  23851  abelthlem8  26682  rpvmasum2  27756  mulog2sumlem2  27779  f1otrge  29336  nn0xmulclb  33250  intlidl  33856  ply1degltdimlem  34140  fedgmul  34149  cos9thpiminplylem2  34301  signstfvneq0  35088  breprexplemc  35148  mblfinlem2  38415  supxrgelem  46175  supxrge  46176  rexabslelem  46254  uzub  46267  smflimlem4  47610  grimcnv  48812  iinfsubc  49992