Theorem ad5ant15 768

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  summolem2  15733  ntrivcvg  15917  xkoccn  23666  abelthlem8  26489  rpvmasum2  27563  mulog2sumlem2  27586  f1otrge  29028  nn0xmulclb  32933  intlidl  33566  ply1degltdimlem  33879  fedgmul  33888  cos9thpiminplylem2  34040  signstfvneq0  34826  breprexplemc  34886  mblfinlem2  38117  supxrgelem  45873  supxrge  45874  rexabslelem  45952  uzub  45965  smflimlem4  47308  grimcnv  48470  iinfsubc  49639