Theorem ad4ant23 750

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fntpb  7085  suppssfv  8018  omsmolem  8487  ttukeylem5  10269  rlim3  15207  mp2pm2mplem4  21958  chfacfisf  22003  chfacfisfcpmat  22004  mbfi1fseqlem3  24882  usgredg2vlem2  27593  umgr3v3e3cycl  28548  matunitlindflem1  35773  matunitlindflem2  35774  heicant  35812  difmap  42747  xlimmnfvlem2  43374  xlimpnfvlem2  43378  xlimliminflimsup  43403  sge0resplit  43944  hoidmvle  44138  eenglngeehlnmlem2  46084