Theorem simpllr 788

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.)

Assertion

Ref	Expression
simpllr	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpllr

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad3antlr 744	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:  frpomin  6336  fsnex  7283  soisoi  7328  f1o2ndf1  8122  fimaproj  8136  fprlem2  8303  tz7.49  8439  omabs  8644  cofon1  8665  naddssim  8679  omxpenlem  9081  fopwdom  9088  findcard3  9258  frfi  9260  finsschain  9332  marypha1lem  9409  wemappo  9527  wdomtr  9553  cantnfp1  9666  ttrcltr  9701  harcard  10040  numacn  10109  infunsdom1  10271  sornom  10336  ssfin4  10369  fin1a2lem11  10469  fin1a2lem13  10471  fpwwe2lem12  10708  pwfseq  10730  mulcmpblnr  11137  00id  11466  addrid  11471  cnegex  11472  negeu  11528  add20  11809  ltmul12a  12154  lediv12a  12191  cru  12293  qextltlem  13313  xleadd1a  13364  xmullem  13375  xlemul1a  13399  ixxss12  13477  ioodisj  13594  fvf1tp  13909  fsuppmapnn0fz  14119  seqf1o  14166  mulexpz  14225  leexp1a  14298  faclbnd  14414  ccatf1  14716  swrdf1  14779  swrdswrdlem  14833  s3rex  15081  sgnsub  15239  abs3lem  15486  rexico  15501  cau3lem  15502  rlim3  15645  ello12  15663  lo1bdd2  15671  elo12  15674  rlimconst  15691  isercoll  15815  climcau  15818  climbdd  15819  summolem2  15862  fsumconst  15936  o1fsum  15960  incexclem  15985  fprodconst  16125  bitsfzo  16585  dvdsmulgcd  16710  pc2dvds  17037  pcz  17039  pcadd  17047  pcfac  17057  vdwmc2  17137  vdwlem2  17140  vdwlem10  17148  vdw  17152  ramcl  17187  sbcie3s  17320  firest  17583  prdsval  17606  mreexd  17796  mreexexlemd  17798  iscat  17826  cidfval  17830  iscatd2  17835  catcocl  17839  catass  17840  catpropd  17863  cidpropd  17864  moni  17891  monpropd  17892  issubc  17990  subccocl  18000  funcco  18026  funcpropd  18057  fullpropd  18077  nati  18113  natpropd  18134  fucpropd  18135  xpcpropd  18362  curfuncf  18392  curf2ndf  18401  yonffthlem  18436  acsfiindd  18707  chnind  18775  chnso  18778  mgmhmeql  18885  sgrppropd  18900  mndpropd  18931  mhmeql  19002  smndex1mgm  19086  isgrpinv  19184  dfgrp3lem  19228  mhmmnd  19254  cycsubm  19397  cycsubmcom  19399  conjnmzb  19447  ghmqusnsg  19476  ghmquskerlem3  19480  ghmqusker  19481  gass  19495  symgextf  19611  dfod2  19758  gexdvds  19778  sylow3lem2  19822  efgredlem  19941  efgredeu  19946  ghmcmn  20025  oddvdssubg  20049  dprdfcntz  20211  pgpfaclem3  20279  gsumle  20339  isrng  20356  issrg  20394  isring  20443  dvdsrmul1  20579  isdrng4  20972  issubdrg  21017  suborng  21113  islmhm2  21293  lmhmeql  21310  lssacsex  21402  rhmpreimaidl  21551  rhmqusnsg  21561  prmidl2  21602  isprmidlc  21608  rhmpreimaprmidl  21615  qsidomlem2  21617  ssdifidllem  21620  ssdifidlprm  21622  isphl  21914  uvcf1  22078  lindfmm  22113  sraassab  22156  issubassa2  22180  opsrval  22335  psdmul  22467  scmatmats  22806  smatvscl  22819  mdetunilem7  22913  gsummatr01lem4  22953  matunitlindflem1  22974  matunitlindflem2  22975  m2cpmfo  23054  pmatcollpw3fi1lem1  23084  pm2mpf1lem  23092  pm2mpf1  23097  mp2pm2mplem4  23107  pm2mpghm  23114  chfacfscmulfsupp  23157  chfacfpmmulfsupp  23161  cctop  23304  neiptoptop  23429  neiptopreu  23431  tgrest  23457  ordtrest2lem  23501  cnss1  23574  cncnp  23578  isnrm3  23657  uncmp  23701  cmpfi  23706  iunconn  23726  1stcrest  23751  subislly  23780  islly2  23783  cldllycmp  23794  lly1stc  23795  llycmpkgen2  23849  kgencn  23855  xkoccn  23918  ptcnplem  23920  pthaus  23937  txhaus  23946  txkgen  23951  xkohaus  23952  xkococnlem  23958  txconn  23988  regr1lem2  24039  kqreglem1  24040  reghmph  24092  nrmhmph  24093  trfil2  24186  ufileu  24218  flimopn  24274  flimcf  24281  fclscf  24324  ufilcmp  24331  cnpfcf  24340  cnextfun  24363  tgpmulg  24392  symgtgp  24405  tgpt0  24418  qustgplem  24420  ustex2sym  24516  ustex3sym  24517  trust  24528  restutop  24536  restutopopn  24537  ustuqtop4  24543  utop3cls  24550  utopreg  24551  cstucnd  24582  ucncn  24583  trcfilu  24592  neipcfilu  24594  ismet2  24632  metequiv2  24809  metcnp  24840  metcnp2  24841  metcnpi3  24845  txmetcnp  24846  metustto  24852  metustsym  24854  metust  24857  cfilucfil  24858  metuel2  24864  psmetutop  24866  restmetu  24869  metucn  24870  ngptgp  24935  tngngp  24953  nmoleub  25030  icccmp  25125  reconnlem2  25127  reconn  25128  xmetdcn2  25137  metdseq0  25154  metdscn  25156  elcncf2  25191  cncfmet  25210  cnheibor  25256  nmoleub2lem2  25417  nmoleub3  25420  cvsi  25431  iscfil2  25567  iscfil3  25574  cfilfcls  25575  equivcfil  25600  caubl  25609  bcthlem5  25629  pmltpc  25751  ovollb2  25790  ovoliunnul  25808  ovolicc2lem4  25821  volsup  25857  ioorf  25874  dyadss  25895  dyaddisjlem  25896  mbfposr  25953  cncombf  25959  mbflimsup  25967  i1fmulclem  26003  mbfi1fseqlem4  26019  iblss2  26106  ellimc2  26177  ellimc3  26179  dvnadd  26229  dvmptfsum  26275  dvferm1  26285  dvferm2  26287  fta1g  26468  plyeq0lem  26509  plydivex  26600  fta1  26611  aalioulem2  26642  aalioulem3  26643  ulmuni  26701  ulmbdd  26707  ulmdvlem3  26711  mtest  26713  abelthlem8  26748  efopn  26968  cxpmul2z  27001  cxpcn3lem  27057  jensen  27298  lgambdd  27346  lgamucov  27347  isppw2  27424  mersenne  27536  dchrelbas3  27547  dchrptlem1  27573  dchrpt  27576  lgsval2lem  27616  lgsdchrval  27663  lgsquad3  27696  2sqb  27741  2sqmo  27746  pntrsumbnd2  27876  pntpbnd  27897  pntibnd  27902  nna4b4nsq  27972  nosupno  28042  noinfno  28057  noetasuplem4  28075  noetalem1  28080  madebday  28268  cofcutr  28292  negsprop  28403  mulscom  28507  absmuls  28612  addonbday  28647  bdayfinbndlem1  28835  z12sge0  28851  remulscl  28870  tgjustr  28918  tgsegconeu  28931  tglowdim1i  28946  tgbtwndiff  28951  tgifscgr  28953  iscgrglt  28959  tgcgrxfr  28963  lnext  29012  tgbtwnconn1lem3  29019  tgbtwnconn1  29020  legval  29029  legov  29030  legov2  29031  legtrd  29034  legtri3  29035  legso  29044  hlcgrex  29064  hlcgreu  29066  tglnne  29078  tglndim0  29079  tglineeltr  29081  tglinethru  29086  tglinesseq  29090  tglnne0  29091  colline  29100  tglowdim2l  29101  tglowdim2ln  29102  tglnpt2  29103  tglnpt3  29104  tglnpt4  29105  mirreu3  29108  miriso  29124  midexlem  29146  isperp  29169  perpcom  29170  perpneq  29171  isperp2  29172  footexALT  29175  footex  29178  colperpexlem3  29190  opphllem  29193  midex  29195  oppne3  29201  opptgdim2  29203  opphllem2  29206  opphllem3  29207  opphllem5  29209  opphllem6  29210  opphl  29212  outpasch  29215  lnopp2hpgb  29223  colopp  29229  plngrnssp  29239  lnincplng  29244  plngrotlem1  29247  plngrotlem3  29249  lnssplng  29252  plng3p  29257  lmieu  29271  trgcopy  29293  trgcopyeu  29295  iscgra1  29299  cgrane1  29301  cgrane2  29302  cgrane3  29303  cgrahl1  29305  cgrahl2  29306  cgracgr  29307  cgraswap  29309  cgracom  29311  cgratr  29312  zerocgra  29313  flatcgra  29314  cgrabtwn  29316  cgrahl  29317  dfcgra2  29320  sacgr  29321  acopyeu  29324  ragcgra  29325  cgrarag  29326  ragsupplcgra  29327  tgaaddcpbllem1  29331  tgaaddcpbllem3  29333  tgaaddcpbl  29334  inaghl  29346  cgrg3col4  29354  cgraer  29359  cgrabasimass  29360  angmgmaddeu1  29361  angmgmaddeu2  29362  angmgmaddeu3  29363  angmgmaddeu4  29364  angmgmaddeu5  29365  angmgmaddeu6  29366  angmgmaddeu7  29367  angmgmaddov2lem  29369  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddlid  29374  angmgmaddrid  29375  angmgm  29379  prlnghpg  29406  dfprlng2  29407  dfprlng3  29408  perpprlng  29410  prlngex  29411  prlngmolem1  29412  prlngmolem2  29413  prlngmo2  29416  prlngplngtr  29419  quadcgrprlng  29426  f1otrg  29430  f1otrge  29431  axsegcon  29487  axeuclidlem  29522  upgr1eopALT  29677  usgr1eop  29813  pthdepisspth  30303  wpthswwlks2on  30535  clwwlkf1  30622  clwwlknscsh  30635  2pthfrgr  30867  n4cyclfrgr  30874  frgrwopreglem5  30904  frgrwopreglem5ALT  30905  friendshipgt3  30981  smcnlem  31281  0lno  31374  ubthlem1  31454  ubthlem3  31456  chocunii  31885  occl  31888  5oalem1  32238  3oalem2  32247  nmopub2tALT  32493  nmfnleub2  32510  lnconi  32617  kbass5  32704  mdslmd1lem1  32909  mdslmd1lem2  32910  cdj1i  33017  opreu2reuALT  33055  disjabrex  33158  disjabrexf  33159  2ndresdju  33225  acunirnmpt  33235  acunirnmpt2  33236  acunirnmpt2f  33237  aciunf1lem  33238  fnpreimac  33246  fgreu  33247  suppovss  33256  xrge0infss  33334  xrofsup  33341  elq2  33385  fsumiunle  33402  2exple2exp  33407  s3f1  33493  ccatws1f1o  33496  ressprs  33509  dfmgc2  33539  mgcf1o  33546  xrge0addgt0  33560  mndlrinvb  33568  mndlactf1  33569  mndlactfo  33570  mndractf1  33571  mndractfo  33572  mndlactf1o  33573  gsumfs2d  33604  suppgsumssiun  33615  gsumwun  33619  gsumwrd2dccatlem  33620  psgnfzto1stlem  33643  fzto1st1  33645  cycpmco2  33676  cycpmrn  33686  cyc3genpm  33695  cycpmconjs  33699  cyc3conja  33700  conjga  33713  fxpsubrg  33717  submarchi  33729  isarchi3  33730  archiabllem1  33736  archiabllem2a  33737  isarchiofld  33742  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnlem4  33788  elrgspnsubrunlem2  33791  erler  33808  rlocaddval  33812  rlocmulval  33813  rloccring  33814  rloc1r  33816  rlocisunit  33819  subrdom  33828  ricdomn1  33832  fracfld  33852  imaslmod  33896  dvdsruasso  33922  unitprodclb  33926  nsgqusf1olem2  33947  lmhmqusker  33950  intlidl  33952  rhmquskerlem  33957  elrspunidl  33960  elrspunsn  33961  rhmimaidl  33964  mxidlprm  33977  ssmxidl  33981  opprqusplusg  33995  opprqusmulr  33997  qsdrngilem  34000  qsdrngi  34001  drnglring  34006  dflring2  34007  dflringlem2  34009  rsprprmprmidl  34036  rsprprmprmidlb  34037  rprmirred  34045  rprmirredb  34046  rprmdvdspow  34047  rprmdvdsprod  34048  1arithidom  34051  1arithufdlem2  34059  1arithufdlem3  34060  1arithufdlem4  34061  dfufd2lem  34063  dfufd2  34064  zringfrac  34068  deg1prod  34097  ply1dg3rt0irred  34098  r1plmhm  34123  r1pquslmic  34124  0mplrim  34128  mplidomlem  34141  extvfvcl  34150  mplmulmvr  34153  mplvrpmga  34159  psrgsum  34162  psrmonprod  34166  esplyfval3  34186  esplyfval1  34187  esplyfvaln  34188  esplyind  34189  exsslsb  34211  lindsunlem  34238  lindsun  34239  dimkerim  34241  fedgmullem1  34243  fedgmul  34245  dimlssid  34246  evls1fldgencl  34284  fldextrspunlsplem  34287  extdgfialg  34308  minplyirred  34325  fldext2chn  34342  constrmon  34358  constrconj  34359  constrfin  34360  constrelextdg2  34361  constrextdg2lem  34362  constrextdg2  34363  constrext2chnlem  34364  constrfiss  34365  cos9thpiminplylem2  34397  mdetpmtr1  34437  txomap  34448  qtophaus  34450  cmpcref  34464  zarclsun  34484  zarclssn  34487  zarcmplem  34495  pstmxmet  34511  sqsscirc1  34522  ordtrest2NEWlem  34536  ordtconnlem1  34538  pnfneige0  34565  lmxrge0  34566  lmdvg  34567  qqhval2  34596  esumcst  34677  esumrnmpt2  34682  esumfsup  34684  esumcvg  34700  esum2d  34707  esumiun  34708  sigaclfu2  34735  insiga  34752  ldsysgenld  34775  ldgenpisyslem1  34778  fiunelros  34789  measinb  34836  imambfm  34877  oms0  34912  omssubadd  34915  carsgclctunlem3  34935  eulerpartlemgvv  34991  dstrvprob  35087  signstfvneq0  35184  actfunsnrndisj  35217  reprinfz1  35234  breprexp  35245  afsval  35286  derangenlem  35905  sconnpi1  35973  cvmsss2  36008  cvmopnlem  36012  cvmlift3lem7  36059  msrval  36272  ifscgr  36779  cgrxfr  36790  btwnconn1lem13  36834  outsideofeu  36866  nmulcom  36913  nmuladdss  36932  neibastop2lem  37118  weiunso  37224  mh-inf3f1  37299  irrdifflemf  38214  irrdiff  38215  poimirlem14  38520  poimirlem22  38528  poimirlem29  38535  broucube  38540  heicant  38541  mblfinlem1  38543  itg2addnclem  38557  ftc1cnnc  38578  ftc1anclem7  38585  sstotbnd2  38676  equivtotbnd  38680  isbnd3  38686  ssbnd  38690  totbndbnd  38691  cntotbnd  38698  heibor1lem  38711  rrncmslem  38734  lssats  40037  lsat0cv  40058  lkrlss  40120  lfl1dim  40146  lfl1dim2N  40147  lkrpssN  40188  hlhgt2  40414  3dim2  40493  2dim  40495  lplncvrlvol  40641  paddasslem11  40855  pmapjat1  40878  2polssN  40940  pclfinclN  40975  pexmidlem8N  41002  lhpexle1lem  41032  4atex  41101  ltrnid  41160  trlator0  41196  cdlemg2cex  41616  tendodi1  41809  tendodi2  41810  diblss  42195  dihopelvalcpre  42273  dihatexv  42363  mapdval4N  42657  fldhmf1  43108  mndmolinv  43113  primrootscoprmpow  43117  posbezout  43118  primrootscoprbij2  43121  primrootspoweq0  43124  aks6d1c2p2  43137  hashscontpow  43140  aks6d1c2lem4  43145  aks6d1c2  43148  aks6d1c5  43157  sticksstones8  43171  sticksstones12  43176  sticksstones22  43186  aks6d1c6lem3  43190  aks6d1c6isolem1  43192  unitscyglem3  43215  aks5  43222  sn-subeu  43446  sn-0tie0  43483  fiabv  43562  frlmsnic  43566  fsuppind  43580  prjspersym  43597  dffltz  43624  mzpindd  43710  mzpsubst  43712  mzpcompact2lem  43715  eldioph2b  43727  irrapxlem3  43784  irrapxlem5  43786  pellex  43795  pell1234qrdich  43821  pell14qrexpcl  43827  congabseq  43934  jm2.26a  43960  jm2.26lem3  43961  rmydioph  43974  lnrfg  44079  hbt  44090  cantnftermord  44280  cantnfresb  44284  cantnf2  44285  oawordex2  44286  omabs2  44292  tfsconcatfv  44301  tfsconcatrev  44308  ofoaass  44320  nadd2rabtr  44344  nadd1suc  44352  naddgeoa  44354  rfovcnvf1od  44963  clsk3nimkb  44999  ntrneiiso  45050  ntrneikb  45053  ntrneixb  45054  ntrneik3  45055  ntrneix3  45056  ntrneik13  45057  ntrneix13  45058  4an4132  45441  iunconnlem2  45876  modelaxrep  45923  fnchoice  45989  cncmpmax  45992  ssinc  46045  ssdec  46046  disjf1  46141  supxrge  46294  suplesup  46295  infxr  46322  infleinf  46327  unb2ltle  46369  rexabslelem  46372  uzub  46385  supminfxr  46418  climrec  46559  climsuse  46564  islptre  46575  addlimc  46602  0ellimcdiv  46603  limsuppnfdlem  46655  limsupub  46658  limsuppnflem  46664  limsupubuz  46667  climinf3  46670  limsupmnflem  46674  climxrre  46704  liminfreuzlem  46756  liminflimsupclim  46761  xlimliminflimsup  46816  icccncfext  46841  cncfiooicclem1  46847  fperdvper  46873  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvmptfprodlem  46898  dvmptfprod  46899  dvnprodlem2  46901  stoweidlem7  46961  stoweidlem34  46988  stoweidlem52  47006  stoweidlem60  47014  wallispilem3  47021  fourierdlem34  47095  fourierdlem38  47099  fourierdlem39  47100  fourierdlem48  47108  fourierdlem50  47110  fourierdlem51  47111  fourierdlem73  47133  fourierdlem76  47136  fourierdlem77  47137  fourierdlem80  47140  fourierdlem87  47147  fourierdlem103  47163  fourierdlem104  47164  etransclem32  47220  etransclem33  47221  sge0f1o  47336  sge0pr  47348  sge0isum  47381  iundjiun  47414  meaiininclem  47440  hoicvr  47502  pimdecfgtioo  47671  pimincfltioo  47672  preimageiingt  47674  preimaleiinlt  47675  smflimlem2  47726  smflimlem4  47728  smfmullem3  47747  smflimmpt  47764  smfinflem  47771  smfpimne2  47794  fsupdm  47796  finfdm  47800  cfsetsnfsetfo  48074  funressnbrafv2  48258  imasetpreimafvbijlemf1  48430  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  bgoldbtbnd  48851  isuspgrim  48938  stgrusgra  49001  isubgr3stgrlem6  49013  2zlidl  49281  lindslinindsimp2  49519  snlindsntor  49527  lincresunit2  49534  islindeps2  49539  imaf1co  50207  imasubc3  50208  fucofvalg  50370  fuco21  50388  precofvalALT  50420  lanfval  50665  ranfval  50666