Theorem ad4ant23 765

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fntpb  7207  suppssfv  8194  omsmolem  8639  ttukeylem5  10492  rlim3  15545  mp2pm2mplem4  22966  chfacfisf  23011  chfacfisfcpmat  23012  mbfi1fseqlem3  25876  usgredg2vlem2  29576  umgr3v3e3cycl  30535  zringfrac  33844  matunitlindflem1  38267  matunitlindflem2  38268  heicant  38306  naddgeoa  44121  difmap  45923  xlimmnfvlem2  46547  xlimpnfvlem2  46551  xlimliminflimsup  46576  sge0resplit  47120  hoidmvle  47314  grimcnv  48653  eenglngeehlnmlem2  49518