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  15639  ntrivcvg  15820  xkoccn  23563  abelthlem8  26405  rpvmasum2  27479  mulog2sumlem2  27502  f1otrge  28944  nn0xmulclb  32851  intlidl  33501  ply1degltdimlem  33779  fedgmul  33788  cos9thpiminplylem2  33940  signstfvneq0  34729  breprexplemc  34789  mblfinlem2  37859  supxrgelem  45582  supxrge  45583  rexabslelem  45662  uzub  45675  smflimlem4  47018  grimcnv  48134  iinfsubc  49303