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  8486  oewordri  8518  naddssim  8611  infxp  10122  lediv12a  12033  xmulgt0  13196  ioodisj  13396  leexp1a  14096  swrdswrdlem  14625  seqshft  15006  sumss2  15647  prmdvdsncoprmbd  16652  mulgfval  18997  grpissubg  19074  f1otrspeq  19374  mat1dimcrng  22419  elcls  23015  neiptopreu  23075  alexsubALTlem4  23992  ustuqtop2  24184  iscfil2  25220  absmuls  28212  tglowdim1i  28522  axcontlem2  28987  opreu2reuALT  32500  nsgqusf1olem1  33443  lbslelsp  33703  matunitlindflem1  37756  matunitlindflem2  37757  poimirlem4  37764  founiiun0  45376  xralrple2  45541  rexabslelem  45604  climisp  45932  climxrre  45936  cnrefiisplem  46015  sge0iunmptlemre  46601  nnfoctbdjlem  46641  iundjiun  46646  meaiuninc3v  46670  hoidmvlelem3  46783  hspmbllem2  46813  smflimlem2  46958