Theorem ad4ant23 750

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 715	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 206  df-an 396

This theorem is referenced by:  fntpb  7213  suppssfv  8190  omsmolem  8659  ttukeylem5  10511  rlim3  15447  mp2pm2mplem4  22532  chfacfisf  22577  chfacfisfcpmat  22578  mbfi1fseqlem3  25468  usgredg2vlem2  28751  umgr3v3e3cycl  29705  matunitlindflem1  36788  matunitlindflem2  36789  heicant  36827  naddgeoa  42448  difmap  44205  xlimmnfvlem2  44848  xlimpnfvlem2  44852  xlimliminflimsup  44877  sge0resplit  45421  hoidmvle  45615  eenglngeehlnmlem2  47512