Theorem ad5ant15 764

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  summolem2  15676  ntrivcvg  15860  xkoccn  23609  abelthlem8  26429  rpvmasum2  27500  mulog2sumlem2  27523  f1otrge  28965  nn0xmulclb  32870  intlidl  33510  ply1degltdimlem  33813  fedgmul  33822  cos9thpiminplylem2  33974  signstfvneq0  34763  breprexplemc  34823  mblfinlem2  38032  supxrgelem  45789  supxrge  45790  rexabslelem  45868  uzub  45881  smflimlem4  47224  grimcnv  48386  iinfsubc  49555