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  7183  suppssfv  8181  omsmolem  8621  ttukeylem5  10466  rlim3  15464  mp2pm2mplem4  22696  chfacfisf  22741  chfacfisfcpmat  22742  mbfi1fseqlem3  25618  usgredg2vlem2  29153  umgr3v3e3cycl  30113  zringfrac  33525  matunitlindflem1  37610  matunitlindflem2  37611  heicant  37649  naddgeoa  43383  difmap  45201  xlimmnfvlem2  45831  xlimpnfvlem2  45835  xlimliminflimsup  45860  sge0resplit  46404  hoidmvle  46598  grimcnv  47885  eenglngeehlnmlem2  48724