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  7230  suppssfv  8228  omsmolem  8696  ttukeylem5  10554  rlim3  15535  mp2pm2mplem4  22816  chfacfisf  22861  chfacfisfcpmat  22862  mbfi1fseqlem3  25753  usgredg2vlem2  29244  umgr3v3e3cycl  30204  zringfrac  33583  matunitlindflem1  37624  matunitlindflem2  37625  heicant  37663  naddgeoa  43412  difmap  45217  xlimmnfvlem2  45853  xlimpnfvlem2  45857  xlimliminflimsup  45882  sge0resplit  46426  hoidmvle  46620  grimcnv  47884  eenglngeehlnmlem2  48664