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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  fntpb  7228  suppssfv  8219  omsmolem  8689  ttukeylem5  10558  rlim3  15502  mp2pm2mplem4  22805  chfacfisf  22850  chfacfisfcpmat  22851  mbfi1fseqlem3  25741  usgredg2vlem2  29165  umgr3v3e3cycl  30120  zringfrac  33431  matunitlindflem1  37319  matunitlindflem2  37320  heicant  37358  naddgeoa  43079  difmap  44832  xlimmnfvlem2  45472  xlimpnfvlem2  45476  xlimliminflimsup  45501  sge0resplit  46045  hoidmvle  46239  grimcnv  47476  eenglngeehlnmlem2  48144