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  7338  dfac9  10220  lediv12a  12215  leexp1a  14323  seqcoll  14614  ccatf1  14741  lo1bdd2  15698  rlimcld2  15752  rlimcn1  15762  isercolllem1  15839  summo  15890  climcnds  16027  geomulcvg  16052  mertenslem2  16061  prodmolem2  16109  prodmo  16110  fprod2d  16155  pwsle  17671  isacs2  17834  grpinvalem  18861  gsumpropd2lem  18875  gsumwsubmcl  19040  gsumwmhm  19048  mulgfval  19286  gaid  19520  gsmsymgrfixlem1  19648  mulgnn0di  20046  gsumval3  20128  subrngint  20819  matunitlindflem1  23001  matunitlindflem2  23002  fvmptnn04if  23174  cnpnei  23589  lfinun  23851  xkopt  23981  isr0  24063  fbflim  24302  alexsubALTlem3  24375  metss  24834  iscmet3lem2  25620  ovoliunlem3  25832  mbfposr  25980  i1fmulclem  26030  itg10a  26038  iblss  26132  dvlip  26320  plyeq0lem  26536  mtest  26738  itgulm  26742  dchrisumlem3  27825  rpvmasum2  27846  pntlem3  27943  nosupbday  28069  noinfbday  28084  addonbday  28672  hlpasch  29241  f1otrg  29455  lfgrwlkprop  30277  wlkiswwlks1  30463  frgrnbnb  30901  frgr2wwlkeqm  30939  unidifsnne  33181  hashxpe  33447  fxpsubm  33781  fxpsubrg  33783  mplvrpmmhm  34226  mplvrpmrhm  34227  esplyfval1  34253  vieta  34260  cos9thpiminplylem1  34462  omssubadd  34980  signstfvneq0  35249  bnj605  35585  poimirlem26  38671  mblfinlem2  38683  ssfiunibd  46432  xralrple2  46473  infleinf  46490  infxrpnf  46563  fprodcn  46719  limsupub  46821  limsuppnflem  46827  limsupmnflem  46837  cnrefiisplem  46946  climxlim2lem  46962  icccncfext  47004  cncficcgt0  47005  cncfioobd  47014  dvbdfbdioolem2  47046  dvmptfprod  47062  itgspltprt  47096  stoweidlem34  47151  stoweidlem49  47166  stoweidlem57  47174  fourierdlem34  47258  fourierdlem39  47263  fourierdlem50  47273  fourierdlem51  47274  fourierdlem64  47287  fourierdlem73  47296  fourierdlem77  47300  fourierdlem81  47304  fourierdlem94  47317  fourierdlem97  47320  fourierdlem103  47326  fourierdlem104  47327  fourierdlem113  47336  fourier2  47344  etransclem24  47375  intsal  47447  sge0pr  47511  sge0iunmptlemfi  47530  sge0seq  47563  sge0reuz  47564  nnfoctbdjlem  47572  meadjiunlem  47582  ismeannd  47584  carageniuncllem2  47639  isomennd  47648  hoicvr  47665  hspmbllem2  47744  iunhoiioolem  47792  iunhoiioo  47793  vonioo  47799  vonicc  47802  preimageiingt  47837  preimaleiinlt  47838  smfaddlem1  47880  smfaddlem2  47881  smflimlem4  47891  smfrec  47906  smfinflem  47934  sprsymrelf1lem  48680  lighneallem3  48799  1arymaptfo  49862