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  7246  suppssfv  8257  omsmolem  8704  ttukeylem5  10630  rlim3  15709  matunitlindflem1  23049  matunitlindflem2  23050  mp2pm2mplem4  23182  chfacfisf  23227  chfacfisfcpmat  23228  mbfi1fseqlem3  26093  usgredg2vlem2  29864  umgr3v3e3cycl  30842  zringfrac  34189  heicant  38841  naddgeoa  44657  difmap  46493  xlimmnfvlem2  47116  xlimpnfvlem2  47120  xlimliminflimsup  47145  sge0resplit  47689  hoidmvle  47883  grimcnv  49259  eenglngeehlnmlem2  50182