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  7138  suppssfv  8127  omsmolem  8567  ttukeylem5  10399  rlim3  15400  mp2pm2mplem4  22719  chfacfisf  22764  chfacfisfcpmat  22765  mbfi1fseqlem3  25640  usgredg2vlem2  29199  umgr3v3e3cycl  30156  zringfrac  33511  matunitlindflem1  37656  matunitlindflem2  37657  heicant  37695  naddgeoa  43427  difmap  45244  xlimmnfvlem2  45871  xlimpnfvlem2  45875  xlimliminflimsup  45900  sge0resplit  46444  hoidmvle  46638  grimcnv  47919  eenglngeehlnmlem2  48770