Theorem ad5ant15 770

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 727	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	ad4ant14 764	1 ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  summolem2  15769  ntrivcvg  15953  xkoccn  23757  abelthlem8  26583  rpvmasum2  27657  mulog2sumlem2  27680  f1otrge  29202  nn0xmulclb  33097  intlidl  33709  ply1degltdimlem  33993  fedgmul  34002  cos9thpiminplylem2  34154  signstfvneq0  34940  breprexplemc  35000  mblfinlem2  38290  supxrgelem  46036  supxrge  46037  rexabslelem  46115  uzub  46128  smflimlem4  47471  grimcnv  48636  iinfsubc  49819