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  15755  ntrivcvg  15939  xkoccn  23733  abelthlem8  26556  rpvmasum2  27630  mulog2sumlem2  27653  f1otrge  29126  nn0xmulclb  33024  intlidl  33639  ply1degltdimlem  33924  fedgmul  33933  cos9thpiminplylem2  34085  signstfvneq0  34871  breprexplemc  34931  mblfinlem2  38164  supxrgelem  45912  supxrge  45913  rexabslelem  45991  uzub  46004  smflimlem4  47347  grimcnv  48509  iinfsubc  49688