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  8600  oewordri  8631  naddssim  8724  infxp  10255  lediv12a  12162  xmulgt0  13326  ioodisj  13523  leexp1a  14216  swrdswrdlem  14743  seqshft  15125  sumss2  15763  prmdvdsncoprmbd  16765  mulgfval  19088  grpissubg  19165  f1otrspeq  19466  mat1dimcrng  22484  elcls  23082  neiptopreu  23142  alexsubALTlem4  24059  ustuqtop2  24252  iscfil2  25301  absmuls  28269  tglowdim1i  28510  axcontlem2  28981  opreu2reuALT  32497  nsgqusf1olem1  33442  lbslelsp  33649  matunitlindflem1  37624  matunitlindflem2  37625  poimirlem4  37632  founiiun0  45200  xralrple2  45370  rexabslelem  45434  climisp  45766  climxrre  45770  cnrefiisplem  45849  sge0iunmptlemre  46435  nnfoctbdjlem  46475  iundjiun  46480  meaiuninc3v  46504  hoidmvlelem3  46617  hspmbllem2  46647  smflimlem2  46792