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  15651  ntrivcvg  15832  xkoccn  23575  abelthlem8  26417  rpvmasum2  27491  mulog2sumlem2  27514  f1otrge  28956  nn0xmulclb  32861  intlidl  33512  ply1degltdimlem  33799  fedgmul  33808  cos9thpiminplylem2  33960  signstfvneq0  34749  breprexplemc  34809  mblfinlem2  37906  supxrgelem  45693  supxrge  45694  rexabslelem  45773  uzub  45786  smflimlem4  47129  grimcnv  48245  iinfsubc  49414