Theorem ad4ant23 752

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 717	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  7246  suppssfv  8243  omsmolem  8713  ttukeylem5  10582  rlim3  15544  mp2pm2mplem4  22836  chfacfisf  22881  chfacfisfcpmat  22882  mbfi1fseqlem3  25772  usgredg2vlem2  29261  umgr3v3e3cycl  30216  zringfrac  33547  matunitlindflem1  37576  matunitlindflem2  37577  heicant  37615  naddgeoa  43356  difmap  45114  xlimmnfvlem2  45754  xlimpnfvlem2  45758  xlimliminflimsup  45783  sge0resplit  46327  hoidmvle  46521  grimcnv  47763  eenglngeehlnmlem2  48472