Theorem ad4ant23 751

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  fntpb  7145  suppssfv  8092  omsmolem  8562  ttukeylem5  10374  rlim3  15306  mp2pm2mplem4  22063  chfacfisf  22108  chfacfisfcpmat  22109  mbfi1fseqlem3  24987  usgredg2vlem2  27881  umgr3v3e3cycl  28835  matunitlindflem1  35929  matunitlindflem2  35930  heicant  35968  difmap  43126  xlimmnfvlem2  43762  xlimpnfvlem2  43766  xlimliminflimsup  43791  sge0resplit  44333  hoidmvle  44527  eenglngeehlnmlem2  46502