Theorem ad5ant15 758

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  summolem2  15623  ntrivcvg  15804  xkoccn  23535  abelthlem8  26377  rpvmasum2  27451  mulog2sumlem2  27474  f1otrge  28851  nn0xmulclb  32752  intlidl  33383  ply1degltdimlem  33633  fedgmul  33642  cos9thpiminplylem2  33794  signstfvneq0  34583  breprexplemc  34643  mblfinlem2  37704  supxrgelem  45382  supxrge  45383  rexabslelem  45462  uzub  45475  smflimlem4  46818  grimcnv  47925  iinfsubc  49096