Theorem ad4ant14 765

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 728	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 728	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5ant15  771  ad5ant25  774  ad5ant125  1390  soisoi  7329  dfac9  10139  lediv12a  12132  leexp1a  14239  seqcoll  14529  ccatf1  14656  lo1bdd2  15611  rlimcld2  15665  rlimcn1  15675  isercolllem1  15752  summo  15803  climcnds  15940  geomulcvg  15965  mertenslem2  15974  prodmolem2  16022  prodmo  16023  fprod2d  16068  pwsle  17578  isacs2  17741  grpinvalem  18767  gsumpropd2lem  18781  gsumwsubmcl  18946  gsumwmhm  18954  mulgfval  19192  gaid  19426  gsmsymgrfixlem1  19554  mulgnn0di  19952  gsumval3  20034  subrngint  20722  matunitlindflem1  22901  matunitlindflem2  22902  fvmptnn04if  23074  cnpnei  23489  lfinun  23751  xkopt  23881  isr0  23963  fbflim  24202  alexsubALTlem3  24275  metss  24734  iscmet3lem2  25520  ovoliunlem3  25732  mbfposr  25880  i1fmulclem  25930  itg10a  25938  iblss  26032  dvlip  26220  plyeq0lem  26436  mtest  26640  itgulm  26644  dchrisumlem3  27727  rpvmasum2  27748  pntlem3  27845  nosupbday  27941  noinfbday  27956  addonbday  28544  hlpasch  29113  f1otrg  29327  lfgrwlkprop  30149  wlkiswwlks1  30335  frgrnbnb  30773  frgr2wwlkeqm  30811  unidifsnne  33011  hashxpe  33278  fxpsubm  33612  fxpsubrg  33614  mplvrpmmhm  34056  mplvrpmrhm  34057  esplyfval1  34083  vieta  34090  cos9thpiminplylem1  34292  signstfvneq0  35080  bnj605  35416  poimirlem26  38395  mblfinlem2  38407  ssfiunibd  46142  xralrple2  46184  infleinf  46201  infxrpnf  46274  fprodcn  46430  limsupub  46532  limsuppnflem  46538  limsupmnflem  46548  cnrefiisplem  46657  climxlim2lem  46673  icccncfext  46715  cncficcgt0  46716  cncfioobd  46725  dvbdfbdioolem2  46757  dvmptfprod  46773  itgspltprt  46807  stoweidlem34  46862  stoweidlem49  46877  stoweidlem57  46885  fourierdlem34  46969  fourierdlem39  46974  fourierdlem50  46984  fourierdlem51  46985  fourierdlem64  46998  fourierdlem73  47007  fourierdlem77  47011  fourierdlem81  47015  fourierdlem94  47028  fourierdlem97  47031  fourierdlem103  47037  fourierdlem104  47038  fourierdlem113  47047  fourier2  47055  etransclem24  47086  intsal  47158  sge0pr  47222  sge0iunmptlemfi  47241  sge0seq  47274  sge0reuz  47275  nnfoctbdjlem  47283  meadjiunlem  47293  ismeannd  47295  carageniuncllem2  47350  isomennd  47359  hoicvr  47376  hspmbllem2  47455  iunhoiioolem  47503  iunhoiioo  47504  vonioo  47510  vonicc  47513  preimageiingt  47548  preimaleiinlt  47549  smfaddlem1  47591  smfaddlem2  47592  smflimlem4  47602  smfrec  47617  smfinflem  47645  sprsymrelf1lem  48391  lighneallem3  48510  1arymaptfo  49573