Theorem ad4ant23 754

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 719	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  7157  suppssfv  8145  omsmolem  8586  ttukeylem5  10426  rlim3  15451  mp2pm2mplem4  22784  chfacfisf  22829  chfacfisfcpmat  22830  mbfi1fseqlem3  25694  usgredg2vlem2  29309  umgr3v3e3cycl  30269  zringfrac  33629  matunitlindflem1  37951  matunitlindflem2  37952  heicant  37990  naddgeoa  43840  difmap  45654  xlimmnfvlem2  46279  xlimpnfvlem2  46283  xlimliminflimsup  46308  sge0resplit  46852  hoidmvle  47046  grimcnv  48376  eenglngeehlnmlem2  49226