Theorem ad5ant15 759

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 716	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	ad4ant14 753	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  15669  ntrivcvg  15853  xkoccn  23594  abelthlem8  26417  rpvmasum2  27489  mulog2sumlem2  27512  f1otrge  28954  nn0xmulclb  32859  intlidl  33495  ply1degltdimlem  33782  fedgmul  33791  cos9thpiminplylem2  33943  signstfvneq0  34732  breprexplemc  34792  mblfinlem2  37993  supxrgelem  45785  supxrge  45786  rexabslelem  45864  uzub  45877  smflimlem4  47220  grimcnv  48376  iinfsubc  49545