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  7208  suppssfv  8200  omsmolem  8645  ttukeylem5  10515  rlim3  15585  matunitlindflem1  22901  matunitlindflem2  22902  mp2pm2mplem4  23034  chfacfisf  23079  chfacfisfcpmat  23080  mbfi1fseqlem3  25945  usgredg2vlem2  29686  umgr3v3e3cycl  30664  zringfrac  33964  heicant  38404  naddgeoa  44235  difmap  46037  xlimmnfvlem2  46661  xlimpnfvlem2  46665  xlimliminflimsup  46690  sge0resplit  47234  hoidmvle  47428  grimcnv  48804  eenglngeehlnmlem2  49668