Theorem ad4ant23 754

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad4ant23	⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Proof of Theorem ad4ant23

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantr 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantlll 719	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:  fntpb  7164  suppssfv  8152  omsmolem  8593  ttukeylem5  10435  rlim3  15460  mp2pm2mplem4  22774  chfacfisf  22819  chfacfisfcpmat  22820  mbfi1fseqlem3  25684  usgredg2vlem2  29295  umgr3v3e3cycl  30254  zringfrac  33614  matunitlindflem1  37937  matunitlindflem2  37938  heicant  37976  naddgeoa  43822  difmap  45636  xlimmnfvlem2  46261  xlimpnfvlem2  46265  xlimliminflimsup  46290  sge0resplit  46834  hoidmvle  47028  grimcnv  48364  eenglngeehlnmlem2  49214