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  15627  ntrivcvg  15808  xkoccn  23537  abelthlem8  26379  rpvmasum2  27453  mulog2sumlem2  27476  f1otrge  28853  nn0xmulclb  32760  intlidl  33394  ply1degltdimlem  33658  fedgmul  33667  cos9thpiminplylem2  33819  signstfvneq0  34608  breprexplemc  34668  mblfinlem2  37721  supxrgelem  45463  supxrge  45464  rexabslelem  45543  uzub  45556  smflimlem4  46899  grimcnv  48015  iinfsubc  49186