Theorem ad4ant24 754

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
ad4ant24	⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant24

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 715	. 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:  oaass  8502  oewordri  8533  naddssim  8626  infxp  10143  lediv12a  12052  xmulgt0  13219  ioodisj  13419  leexp1a  14116  swrdswrdlem  14645  seqshft  15027  sumss2  15668  prmdvdsncoprmbd  16673  mulgfval  18983  grpissubg  19060  f1otrspeq  19361  mat1dimcrng  22397  elcls  22993  neiptopreu  23053  alexsubALTlem4  23970  ustuqtop2  24163  iscfil2  25199  absmuls  28186  tglowdim1i  28481  axcontlem2  28945  opreu2reuALT  32456  nsgqusf1olem1  33377  lbslelsp  33586  matunitlindflem1  37603  matunitlindflem2  37604  poimirlem4  37611  founiiun0  45177  xralrple2  45343  rexabslelem  45407  climisp  45737  climxrre  45741  cnrefiisplem  45820  sge0iunmptlemre  46406  nnfoctbdjlem  46446  iundjiun  46451  meaiuninc3v  46475  hoidmvlelem3  46588  hspmbllem2  46618  smflimlem2  46763