Theorem ad4ant23 765

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 485	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantlll 730	1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fntpb  7208  suppssfv  8197  omsmolem  8642  ttukeylem5  10496  rlim3  15548  mp2pm2mplem4  22934  chfacfisf  22979  chfacfisfcpmat  22980  mbfi1fseqlem3  25844  usgredg2vlem2  29516  umgr3v3e3cycl  30475  zringfrac  33788  matunitlindflem1  38154  matunitlindflem2  38155  heicant  38193  naddgeoa  44012  difmap  45814  xlimmnfvlem2  46438  xlimpnfvlem2  46442  xlimliminflimsup  46467  sge0resplit  47011  hoidmvle  47205  grimcnv  48541  eenglngeehlnmlem2  49402