Theorem ad4ant23 763

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  fntpb  7188  suppssfv  8176  omsmolem  8621  ttukeylem5  10464  rlim3  15516  mp2pm2mplem4  22857  chfacfisf  22902  chfacfisfcpmat  22903  mbfi1fseqlem3  25767  usgredg2vlem2  29384  umgr3v3e3cycl  30343  zringfrac  33711  matunitlindflem1  38076  matunitlindflem2  38077  heicant  38115  naddgeoa  43932  difmap  45744  xlimmnfvlem2  46368  xlimpnfvlem2  46372  xlimliminflimsup  46397  sge0resplit  46941  hoidmvle  47135  grimcnv  48471  eenglngeehlnmlem2  49321