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  7229  suppssfv  8226  omsmolem  8694  ttukeylem5  10551  rlim3  15531  mp2pm2mplem4  22831  chfacfisf  22876  chfacfisfcpmat  22877  mbfi1fseqlem3  25767  usgredg2vlem2  29258  umgr3v3e3cycl  30213  zringfrac  33562  matunitlindflem1  37603  matunitlindflem2  37604  heicant  37642  naddgeoa  43384  difmap  45150  xlimmnfvlem2  45789  xlimpnfvlem2  45793  xlimliminflimsup  45818  sge0resplit  46362  hoidmvle  46556  grimcnv  47817  eenglngeehlnmlem2  48588