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 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantlll 718	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 207  df-an 396

This theorem is referenced by:  fntpb  7145  suppssfv  8135  omsmolem  8575  ttukeylem5  10407  rlim3  15405  mp2pm2mplem4  22694  chfacfisf  22739  chfacfisfcpmat  22740  mbfi1fseqlem3  25616  usgredg2vlem2  29171  umgr3v3e3cycl  30128  zringfrac  33491  matunitlindflem1  37596  matunitlindflem2  37597  heicant  37635  naddgeoa  43367  difmap  45185  xlimmnfvlem2  45814  xlimpnfvlem2  45818  xlimliminflimsup  45843  sge0resplit  46387  hoidmvle  46581  grimcnv  47872  eenglngeehlnmlem2  48723