Theorem ad5ant15 771

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  summolem2  15914  ntrivcvg  16098  xkoccn  23971  abelthlem8  26799  rpvmasum2  27872  mulog2sumlem2  27895  f1otrge  29482  nn0xmulclb  33436  intlidl  34054  ply1degltdimlem  34337  fedgmul  34346  cos9thpiminplylem2  34498  omssubadd  35015  signstfvneq0  35284  breprexplemc  35344  mblfinlem2  38781  supxrgelem  46564  supxrge  46565  rexabslelem  46643  uzub  46656  smflimlem4  47999  grimcnv  49201  iinfsubc  50387