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  7152  suppssfv  8141  omsmolem  8581  ttukeylem5  10415  rlim3  15412  mp2pm2mplem4  22744  chfacfisf  22789  chfacfisfcpmat  22790  mbfi1fseqlem3  25665  usgredg2vlem2  29225  umgr3v3e3cycl  30185  zringfrac  33563  matunitlindflem1  37729  matunitlindflem2  37730  heicant  37768  naddgeoa  43551  difmap  45367  xlimmnfvlem2  45993  xlimpnfvlem2  45997  xlimliminflimsup  46022  sge0resplit  46566  hoidmvle  46760  grimcnv  48050  eenglngeehlnmlem2  48900