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  7165  suppssfv  8158  omsmolem  8598  ttukeylem5  10442  rlim3  15440  mp2pm2mplem4  22672  chfacfisf  22717  chfacfisfcpmat  22718  mbfi1fseqlem3  25594  usgredg2vlem2  29129  umgr3v3e3cycl  30086  zringfrac  33498  matunitlindflem1  37583  matunitlindflem2  37584  heicant  37622  naddgeoa  43356  difmap  45174  xlimmnfvlem2  45804  xlimpnfvlem2  45808  xlimliminflimsup  45833  sge0resplit  46377  hoidmvle  46571  grimcnv  47861  eenglngeehlnmlem2  48700