Theorem ad4ant23 759

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 481	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantlll 724	1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fntpb  7153  suppssfv  8142  omsmolem  8583  ttukeylem5  10426  rlim3  15451  mp2pm2mplem4  22792  chfacfisf  22837  chfacfisfcpmat  22838  mbfi1fseqlem3  25702  usgredg2vlem2  29313  umgr3v3e3cycl  30272  zringfrac  33637  matunitlindflem1  37983  matunitlindflem2  37984  heicant  38022  naddgeoa  43839  difmap  45652  xlimmnfvlem2  46276  xlimpnfvlem2  46280  xlimliminflimsup  46305  sge0resplit  46849  hoidmvle  47043  grimcnv  48379  eenglngeehlnmlem2  49229