Theorem ad4ant24 760

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 721	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 724	1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  oaass  8486  oewordri  8518  naddssim  8611  infxp  10127  lediv12a  12040  xmulgt0  13226  ioodisj  13426  leexp1a  14128  swrdswrdlem  14657  seqshft  15038  sumss2  15679  prmdvdsncoprmbd  16688  mulgfval  19036  grpissubg  19113  f1otrspeq  19413  mat1dimcrng  22460  elcls  23056  neiptopreu  23116  alexsubALTlem4  24033  ustuqtop2  24225  iscfil2  25251  absmuls  28254  tglowdim1i  28587  axcontlem2  29052  opreu2reuALT  32564  nsgqusf1olem1  33496  lbslelsp  33782  matunitlindflem1  37983  matunitlindflem2  37984  poimirlem4  37991  founiiun0  45637  xralrple2  45799  rexabslelem  45861  climisp  46189  climxrre  46193  cnrefiisplem  46272  sge0iunmptlemre  46858  nnfoctbdjlem  46898  iundjiun  46903  meaiuninc3v  46927  hoidmvlelem3  47040  hspmbllem2  47070  smflimlem2  47215