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  8598  oewordri  8629  naddssim  8722  infxp  10252  lediv12a  12159  xmulgt0  13322  ioodisj  13519  leexp1a  14212  swrdswrdlem  14739  seqshft  15121  sumss2  15759  prmdvdsncoprmbd  16761  mulgfval  19100  grpissubg  19177  f1otrspeq  19480  mat1dimcrng  22499  elcls  23097  neiptopreu  23157  alexsubALTlem4  24074  ustuqtop2  24267  iscfil2  25314  absmuls  28283  tglowdim1i  28524  axcontlem2  28995  opreu2reuALT  32505  nsgqusf1olem1  33421  matunitlindflem1  37603  matunitlindflem2  37604  poimirlem4  37611  founiiun0  45133  xralrple2  45304  rexabslelem  45368  climisp  45702  climxrre  45706  cnrefiisplem  45785  sge0iunmptlemre  46371  nnfoctbdjlem  46411  iundjiun  46416  meaiuninc3v  46440  hoidmvlelem3  46553  hspmbllem2  46583  smflimlem2  46728