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  8571  oewordri  8602  naddssim  8695  infxp  10226  lediv12a  12133  xmulgt0  13297  ioodisj  13497  leexp1a  14191  swrdswrdlem  14720  seqshft  15102  sumss2  15740  prmdvdsncoprmbd  16744  mulgfval  19050  grpissubg  19127  f1otrspeq  19426  mat1dimcrng  22413  elcls  23009  neiptopreu  23069  alexsubALTlem4  23986  ustuqtop2  24179  iscfil2  25216  absmuls  28185  tglowdim1i  28426  axcontlem2  28890  opreu2reuALT  32404  nsgqusf1olem1  33374  lbslelsp  33583  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem4  37594  founiiun0  45162  xralrple2  45329  rexabslelem  45393  climisp  45723  climxrre  45727  cnrefiisplem  45806  sge0iunmptlemre  46392  nnfoctbdjlem  46432  iundjiun  46437  meaiuninc3v  46461  hoidmvlelem3  46574  hspmbllem2  46604  smflimlem2  46749