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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  fntpb  7164  suppssfv  8138  omsmolem  8608  ttukeylem5  10458  rlim3  15392  mp2pm2mplem4  22195  chfacfisf  22240  chfacfisfcpmat  22241  mbfi1fseqlem3  25119  usgredg2vlem2  28237  umgr3v3e3cycl  29191  matunitlindflem1  36147  matunitlindflem2  36148  heicant  36186  naddgeoa  41788  difmap  43549  xlimmnfvlem2  44194  xlimpnfvlem2  44198  xlimliminflimsup  44223  sge0resplit  44767  hoidmvle  44961  eenglngeehlnmlem2  46944