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  7206  suppssfv  8206  omsmolem  8674  ttukeylem5  10532  rlim3  15519  mp2pm2mplem4  22752  chfacfisf  22797  chfacfisfcpmat  22798  mbfi1fseqlem3  25675  usgredg2vlem2  29210  umgr3v3e3cycl  30170  zringfrac  33574  matunitlindflem1  37645  matunitlindflem2  37646  heicant  37684  naddgeoa  43385  difmap  45198  xlimmnfvlem2  45829  xlimpnfvlem2  45833  xlimliminflimsup  45858  sge0resplit  46402  hoidmvle  46596  grimcnv  47868  eenglngeehlnmlem2  48685