Theorem ad4ant14 753

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 716	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 716	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:  ad5ant15  759  ad5ant25  762  soisoi  7283  dfac9  10059  lediv12a  12049  leexp1a  14137  seqcoll  14426  lo1bdd2  15486  rlimcld2  15540  rlimcn1  15550  isercolllem1  15627  summo  15679  climcnds  15816  geomulcvg  15841  mertenslem2  15850  prodmolem2  15900  prodmo  15901  fprod2d  15946  pwsle  17456  isacs2  17619  grpinvalem  18641  gsumpropd2lem  18647  gsumwsubmcl  18805  gsumwmhm  18813  mulgfval  19045  gaid  19274  gsmsymgrfixlem1  19402  mulgnn0di  19800  gsumval3  19882  subrngint  20537  fvmptnn04if  22814  cnpnei  23229  lfinun  23490  xkopt  23620  isr0  23702  fbflim  23941  alexsubALTlem3  24014  metss  24473  iscmet3lem2  25259  ovoliunlem3  25471  mbfposr  25619  i1fmulclem  25669  itg10a  25677  iblss  25772  dvlip  25960  plyeq0lem  26175  mtest  26369  itgulm  26373  dchrisumlem3  27454  rpvmasum2  27475  pntlem3  27572  nosupbday  27669  noinfbday  27684  addonbday  28271  hlpasch  28824  f1otrg  28939  lfgrwlkprop  29754  wlkiswwlks1  29935  frgrnbnb  30363  frgr2wwlkeqm  30401  unidifsnne  32606  hashxpe  32880  ccatf1  33009  fxpsubm  33233  fxpsubrg  33235  mplvrpmmhm  33690  mplvrpmrhm  33691  esplyfval1  33717  vieta  33724  cos9thpiminplylem1  33926  signstfvneq0  34716  bnj605  35049  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem26  37967  mblfinlem2  37979  ssfiunibd  45742  xralrple2  45784  infleinf  45801  infxrpnf  45874  fprodcn  46030  limsupub  46132  limsuppnflem  46138  limsupmnflem  46148  cnrefiisplem  46257  climxlim2lem  46273  icccncfext  46315  cncficcgt0  46316  cncfioobd  46325  dvbdfbdioolem2  46357  dvmptfprod  46373  itgspltprt  46407  stoweidlem34  46462  stoweidlem49  46477  stoweidlem57  46485  fourierdlem34  46569  fourierdlem39  46574  fourierdlem50  46584  fourierdlem51  46585  fourierdlem64  46598  fourierdlem73  46607  fourierdlem77  46611  fourierdlem81  46615  fourierdlem94  46628  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  fourier2  46655  etransclem24  46686  intsal  46758  sge0pr  46822  sge0iunmptlemfi  46841  sge0seq  46874  sge0reuz  46875  nnfoctbdjlem  46883  meadjiunlem  46893  ismeannd  46895  carageniuncllem2  46950  isomennd  46959  hoicvr  46976  hspmbllem2  47055  iunhoiioolem  47103  iunhoiioo  47104  vonioo  47110  vonicc  47113  preimageiingt  47148  preimaleiinlt  47149  smfaddlem1  47191  smfaddlem2  47192  smflimlem4  47202  smfrec  47217  smfinflem  47245  sprsymrelf1lem  47951  lighneallem3  48070  1arymaptfo  49119