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  15862  ntrivcvg  16046  xkoccn  23918  abelthlem8  26748  rpvmasum2  27821  mulog2sumlem2  27844  f1otrge  29431  nn0xmulclb  33345  intlidl  33952  ply1degltdimlem  34236  fedgmul  34245  cos9thpiminplylem2  34397  signstfvneq0  35184  breprexplemc  35244  mblfinlem2  38544  supxrgelem  46293  supxrge  46294  rexabslelem  46372  uzub  46385  smflimlem4  47728  grimcnv  48930  iinfsubc  50110