Theorem ad4ant23 766

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fntpb  7213  suppssfv  8212  omsmolem  8659  ttukeylem5  10584  rlim3  15658  matunitlindflem1  22987  matunitlindflem2  22988  mp2pm2mplem4  23120  chfacfisf  23165  chfacfisfcpmat  23166  mbfi1fseqlem3  26031  usgredg2vlem2  29800  umgr3v3e3cycl  30778  zringfrac  34079  heicant  38553  naddgeoa  44380  difmap  46189  xlimmnfvlem2  46812  xlimpnfvlem2  46816  xlimliminflimsup  46841  sge0resplit  47385  hoidmvle  47579  grimcnv  48955  eenglngeehlnmlem2  49819