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  7165  suppssfv  8154  omsmolem  8595  ttukeylem5  10435  rlim3  15433  mp2pm2mplem4  22765  chfacfisf  22810  chfacfisfcpmat  22811  mbfi1fseqlem3  25686  usgredg2vlem2  29311  umgr3v3e3cycl  30271  zringfrac  33647  matunitlindflem1  37867  matunitlindflem2  37868  heicant  37906  naddgeoa  43751  difmap  45565  xlimmnfvlem2  46191  xlimpnfvlem2  46195  xlimliminflimsup  46220  sge0resplit  46764  hoidmvle  46958  grimcnv  48248  eenglngeehlnmlem2  49098