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  7138  suppssfv  8127  omsmolem  8567  ttukeylem5  10396  rlim3  15397  mp2pm2mplem4  22717  chfacfisf  22762  chfacfisfcpmat  22763  mbfi1fseqlem3  25638  usgredg2vlem2  29197  umgr3v3e3cycl  30154  zringfrac  33509  matunitlindflem1  37635  matunitlindflem2  37636  heicant  37674  naddgeoa  43406  difmap  45223  xlimmnfvlem2  45850  xlimpnfvlem2  45854  xlimliminflimsup  45879  sge0resplit  46423  hoidmvle  46617  grimcnv  47898  eenglngeehlnmlem2  48749