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  7217  suppssfv  8224  omsmolem  8671  ttukeylem5  10596  rlim3  15672  matunitlindflem1  23001  matunitlindflem2  23002  mp2pm2mplem4  23134  chfacfisf  23179  chfacfisfcpmat  23180  mbfi1fseqlem3  26045  usgredg2vlem2  29814  umgr3v3e3cycl  30792  zringfrac  34134  heicant  38680  naddgeoa  44503  difmap  46327  xlimmnfvlem2  46950  xlimpnfvlem2  46954  xlimliminflimsup  46979  sge0resplit  47523  hoidmvle  47717  grimcnv  49093  eenglngeehlnmlem2  49958