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  15888  ntrivcvg  16072  xkoccn  23944  abelthlem8  26772  rpvmasum2  27845  mulog2sumlem2  27868  f1otrge  29455  nn0xmulclb  33410  intlidl  34017  ply1degltdimlem  34301  fedgmul  34310  cos9thpiminplylem2  34462  omssubadd  34979  signstfvneq0  35248  breprexplemc  35308  mblfinlem2  38670  supxrgelem  46443  supxrge  46444  rexabslelem  46522  uzub  46535  smflimlem4  47878  grimcnv  49080  iinfsubc  50266