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  15793  ntrivcvg  15977  xkoccn  23813  abelthlem8  26639  rpvmasum2  27713  mulog2sumlem2  27736  f1otrge  29258  nn0xmulclb  33153  intlidl  33759  ply1degltdimlem  34043  fedgmul  34052  cos9thpiminplylem2  34204  signstfvneq0  34991  breprexplemc  35051  mblfinlem2  38350  supxrgelem  46094  supxrge  46095  rexabslelem  46173  uzub  46186  smflimlem4  47529  grimcnv  48694  iinfsubc  49877