Theorem ad4ant14 764

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad5ant15  770  ad5ant25  773  ad5ant125  1388  soisoi  7327  dfac9  10119  lediv12a  12107  leexp1a  14210  seqcoll  14500  lo1bdd2  15574  rlimcld2  15628  rlimcn1  15638  isercolllem1  15715  summo  15767  climcnds  15904  geomulcvg  15929  mertenslem2  15938  prodmolem2  15988  prodmo  15989  fprod2d  16034  pwsle  17545  isacs2  17708  grpinvalem  18730  gsumpropd2lem  18736  gsumwsubmcl  18895  gsumwmhm  18903  mulgfval  19134  gaid  19368  gsmsymgrfixlem1  19496  mulgnn0di  19894  gsumval3  19976  subrngint  20644  fvmptnn04if  22974  cnpnei  23389  lfinun  23650  xkopt  23780  isr0  23862  fbflim  24101  alexsubALTlem3  24174  metss  24633  iscmet3lem2  25419  ovoliunlem3  25631  mbfposr  25779  i1fmulclem  25829  itg10a  25837  iblss  25932  dvlip  26120  plyeq0lem  26335  mtest  26532  itgulm  26536  dchrisumlem3  27620  rpvmasum2  27641  pntlem3  27738  nosupbday  27834  noinfbday  27849  addonbday  28437  hlpasch  28996  f1otrg  29160  lfgrwlkprop  29975  wlkiswwlks1  30156  frgrnbnb  30584  frgr2wwlkeqm  30622  unidifsnne  32822  hashxpe  33092  ccatf1  33209  fxpsubm  33432  fxpsubrg  33434  mplvrpmmhm  33880  mplvrpmrhm  33881  esplyfval1  33907  vieta  33914  cos9thpiminplylem1  34116  signstfvneq0  34903  bnj605  35239  matunitlindflem1  38154  matunitlindflem2  38155  poimirlem26  38184  mblfinlem2  38196  ssfiunibd  45919  xralrple2  45961  infleinf  45978  infxrpnf  46051  fprodcn  46207  limsupub  46309  limsuppnflem  46315  limsupmnflem  46325  cnrefiisplem  46434  climxlim2lem  46450  icccncfext  46492  cncficcgt0  46493  cncfioobd  46502  dvbdfbdioolem2  46534  dvmptfprod  46550  itgspltprt  46584  stoweidlem34  46639  stoweidlem49  46654  stoweidlem57  46662  fourierdlem34  46746  fourierdlem39  46751  fourierdlem50  46761  fourierdlem51  46762  fourierdlem64  46775  fourierdlem73  46784  fourierdlem77  46788  fourierdlem81  46792  fourierdlem94  46805  fourierdlem97  46808  fourierdlem103  46814  fourierdlem104  46815  fourierdlem113  46824  fourier2  46832  etransclem24  46863  intsal  46935  sge0pr  46999  sge0iunmptlemfi  47018  sge0seq  47051  sge0reuz  47052  nnfoctbdjlem  47060  meadjiunlem  47070  ismeannd  47072  carageniuncllem2  47127  isomennd  47136  hoicvr  47153  hspmbllem2  47232  iunhoiioolem  47280  iunhoiioo  47281  vonioo  47287  vonicc  47290  preimageiingt  47325  preimaleiinlt  47326  smfaddlem1  47368  smfaddlem2  47369  smflimlem4  47379  smfrec  47394  smfinflem  47422  sprsymrelf1lem  48128  lighneallem3  48247  1arymaptfo  49307