Theorem ad4ant23 753

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fntpb  7155  suppssfv  8144  omsmolem  8585  ttukeylem5  10423  rlim3  15421  mp2pm2mplem4  22753  chfacfisf  22798  chfacfisfcpmat  22799  mbfi1fseqlem3  25674  usgredg2vlem2  29299  umgr3v3e3cycl  30259  zringfrac  33635  matunitlindflem1  37817  matunitlindflem2  37818  heicant  37856  naddgeoa  43636  difmap  45451  xlimmnfvlem2  46077  xlimpnfvlem2  46081  xlimliminflimsup  46106  sge0resplit  46650  hoidmvle  46844  grimcnv  48134  eenglngeehlnmlem2  48984