Theorem ad4ant23 751

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  fntpb  6974  suppssfv  7868  omsmolem  8282  ttukeylem5  9937  rlim3  14857  mp2pm2mplem4  21419  chfacfisf  21464  chfacfisfcpmat  21465  mbfi1fseqlem3  24320  usgredg2vlem2  27010  umgr3v3e3cycl  27965  matunitlindflem1  34890  matunitlindflem2  34891  heicant  34929  difmap  41477  xlimmnfvlem2  42121  xlimpnfvlem2  42125  xlimliminflimsup  42150  sge0resplit  42695  hoidmvle  42889  eenglngeehlnmlem2  44732