Theorem ad4ant23 749

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 714	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 206  df-an 396

This theorem is referenced by:  fntpb  7067  suppssfv  7989  omsmolem  8447  ttukeylem5  10200  rlim3  15135  mp2pm2mplem4  21866  chfacfisf  21911  chfacfisfcpmat  21912  mbfi1fseqlem3  24787  usgredg2vlem2  27496  umgr3v3e3cycl  28449  matunitlindflem1  35700  matunitlindflem2  35701  heicant  35739  difmap  42636  xlimmnfvlem2  43264  xlimpnfvlem2  43268  xlimliminflimsup  43293  sge0resplit  43834  hoidmvle  44028  eenglngeehlnmlem2  45972