Theorem ad4ant23 753

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  fntpb  7025  suppssfv  7944  omsmolem  8382  ttukeylem5  10127  rlim3  15059  mp2pm2mplem4  21706  chfacfisf  21751  chfacfisfcpmat  21752  mbfi1fseqlem3  24615  usgredg2vlem2  27314  umgr3v3e3cycl  28267  matunitlindflem1  35510  matunitlindflem2  35511  heicant  35549  difmap  42420  xlimmnfvlem2  43049  xlimpnfvlem2  43053  xlimliminflimsup  43078  sge0resplit  43619  hoidmvle  43813  eenglngeehlnmlem2  45757