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  15678  ntrivcvg  15862  xkoccn  23584  abelthlem8  26404  rpvmasum2  27475  mulog2sumlem2  27498  f1otrge  28940  nn0xmulclb  32844  intlidl  33480  ply1degltdimlem  33766  fedgmul  33775  cos9thpiminplylem2  33927  signstfvneq0  34716  breprexplemc  34776  mblfinlem2  37979  supxrgelem  45767  supxrge  45768  rexabslelem  45846  uzub  45859  smflimlem4  47202  grimcnv  48364  iinfsubc  49533