Theorem ad4ant14 750

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
ad4ant14	⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant14

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 713	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 713	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ad5ant15  757  ad5ant25  760  soisoi  7332  dfac9  10172  lediv12a  12153  leexp1a  14188  seqcoll  14478  lo1bdd2  15521  rlimcld2  15575  rlimcn1  15585  isercolllem1  15664  summo  15716  climcnds  15850  geomulcvg  15875  mertenslem2  15884  prodmolem2  15932  prodmo  15933  fprod2d  15978  pwsle  17502  isacs2  17661  grpinvalem  18661  gsumpropd2lem  18667  gsumwsubmcl  18822  gsumwmhm  18830  mulgfval  19059  gaid  19289  gsmsymgrfixlem1  19421  mulgnn0di  19819  gsumval3  19901  subrngint  20538  fvmptnn04if  22839  cnpnei  23256  lfinun  23517  xkopt  23647  isr0  23729  fbflim  23968  alexsubALTlem3  24041  metss  24505  iscmet3lem2  25308  ovoliunlem3  25521  mbfposr  25669  i1fmulclem  25720  itg10a  25728  iblss  25822  dvlip  26014  plyeq0lem  26234  mtest  26430  itgulm  26434  dchrisumlem3  27517  rpvmasum2  27538  pntlem3  27635  nosupbday  27732  noinfbday  27747  hlpasch  28680  f1otrg  28795  lfgrwlkprop  29621  wlkiswwlks1  29798  frgrnbnb  30223  frgr2wwlkeqm  30261  unidifsnne  32462  hashxpe  32714  ccatf1  32815  signstfvneq0  34431  bnj605  34765  matunitlindflem1  37330  matunitlindflem2  37331  poimirlem26  37360  mblfinlem2  37372  ssfiunibd  44960  xralrple2  45005  infleinf  45023  infxrpnf  45097  fprodcn  45257  limsupub  45361  limsuppnflem  45367  limsupmnflem  45377  cnrefiisplem  45486  climxlim2lem  45502  icccncfext  45544  cncficcgt0  45545  cncfioobd  45554  dvbdfbdioolem2  45586  itgspltprt  45636  stoweidlem34  45691  stoweidlem49  45706  stoweidlem57  45714  fourierdlem34  45798  fourierdlem39  45803  fourierdlem50  45813  fourierdlem51  45814  fourierdlem64  45827  fourierdlem73  45836  fourierdlem77  45840  fourierdlem81  45844  fourierdlem94  45857  fourierdlem97  45860  fourierdlem103  45866  fourierdlem104  45867  fourierdlem113  45876  fourier2  45884  etransclem24  45915  intsal  45987  sge0pr  46051  sge0iunmptlemfi  46070  sge0seq  46103  sge0reuz  46104  nnfoctbdjlem  46112  meadjiunlem  46122  ismeannd  46124  carageniuncllem2  46179  isomennd  46188  hoicvr  46205  hspmbllem2  46284  iunhoiioolem  46332  iunhoiioo  46333  vonioo  46339  vonicc  46342  preimageiingt  46377  preimaleiinlt  46378  smfaddlem1  46420  smfaddlem2  46421  smflimlem4  46431  smfrec  46446  smfinflem  46474  sprsymrelf1lem  47099  lighneallem3  47215  1arymaptfo  48067