Theorem simpllr 787

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 743	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:  frpomin  6331  fsnex  7271  soisoi  7316  f1o2ndf1  8105  fimaproj  8119  fprlem2  8286  tz7.49  8420  omabs  8625  cofon1  8646  naddssim  8660  omxpenlem  9054  fopwdom  9061  findcard3  9231  frfi  9233  finsschain  9304  marypha1lem  9381  wemappo  9499  wdomtr  9525  cantnfp1  9638  ttrcltr  9673  harcard  9952  numacn  10021  infunsdom1  10183  sornom  10249  ssfin4  10282  fin1a2lem11  10382  fin1a2lem13  10384  fpwwe2lem12  10615  pwfseq  10637  mulcmpblnr  11044  00id  11373  addrid  11378  cnegex  11379  negeu  11435  add20  11714  ltmul12a  12062  lediv12a  12099  cru  12201  qextltlem  13219  xleadd1a  13270  xmullem  13281  xlemul1a  13305  ixxss12  13383  ioodisj  13500  fvf1tp  13813  fsuppmapnn0fz  14023  seqf1o  14070  mulexpz  14129  leexp1a  14202  faclbnd  14317  swrdswrdlem  14731  sgnsub  15133  abs3lem  15380  rexico  15395  cau3lem  15396  rlim3  15539  ello12  15557  lo1bdd2  15565  elo12  15568  rlimconst  15585  isercoll  15709  climcau  15712  climbdd  15713  summolem2  15757  fsumconst  15831  o1fsum  15855  incexclem  15880  fprodconst  16022  bitsfzo  16483  dvdsmulgcd  16604  pc2dvds  16929  pcz  16931  pcadd  16939  pcfac  16949  vdwmc2  17029  vdwlem2  17032  vdwlem10  17040  vdw  17044  ramcl  17079  sbcie3s  17212  firest  17475  prdsval  17498  mreexd  17688  mreexexlemd  17690  iscat  17718  cidfval  17722  iscatd2  17727  catcocl  17731  catass  17732  catpropd  17755  cidpropd  17756  moni  17783  monpropd  17784  issubc  17882  subccocl  17892  funcco  17918  funcpropd  17949  fullpropd  17969  nati  18005  natpropd  18026  fucpropd  18027  xpcpropd  18254  curfuncf  18284  curf2ndf  18293  yonffthlem  18328  acsfiindd  18599  chnind  18667  chnso  18670  mgmhmeql  18764  sgrppropd  18779  mndpropd  18807  mhmeql  18875  smndex1mgm  18959  isgrpinv  19050  dfgrp3lem  19095  mhmmnd  19121  cycsubm  19264  cycsubmcom  19266  conjnmzb  19314  ghmqusnsg  19343  ghmquskerlem3  19347  ghmqusker  19348  gass  19362  symgextf  19478  dfod2  19625  gexdvds  19645  sylow3lem2  19689  efgredlem  19808  efgredeu  19813  ghmcmn  19892  oddvdssubg  19916  dprdfcntz  20078  pgpfaclem3  20146  gsumle  20206  isrng  20223  issrg  20261  isring  20310  dvdsrmul1  20442  issubdrg  20852  suborng  20948  islmhm2  21128  lmhmeql  21145  lssacsex  21237  rhmpreimaidl  21378  rhmqusnsg  21387  prmidl2  21428  isprmidlc  21434  rhmpreimaprmidl  21439  qsidomlem2  21441  ssdifidllem  21444  ssdifidlprm  21446  isphl  21738  uvcf1  21902  lindfmm  21937  sraassab  21978  issubassa2  22002  opsrval  22157  psdmul  22289  scmatmats  22629  smatvscl  22642  mdetunilem7  22736  gsummatr01lem4  22776  m2cpmfo  22874  pmatcollpw3fi1lem1  22904  pm2mpf1lem  22912  pm2mpf1  22917  mp2pm2mplem4  22927  pm2mpghm  22934  chfacfscmulfsupp  22977  chfacfpmmulfsupp  22981  cctop  23124  neiptoptop  23249  neiptopreu  23251  tgrest  23277  ordtrest2lem  23321  cnss1  23394  cncnp  23398  isnrm3  23477  uncmp  23521  cmpfi  23526  iunconn  23546  1stcrest  23571  subislly  23599  islly2  23602  cldllycmp  23613  lly1stc  23614  llycmpkgen2  23668  kgencn  23674  xkoccn  23737  ptcnplem  23739  pthaus  23756  txhaus  23765  txkgen  23770  xkohaus  23771  xkococnlem  23777  txconn  23807  regr1lem2  23858  kqreglem1  23859  reghmph  23911  nrmhmph  23912  trfil2  24005  ufileu  24037  flimopn  24093  flimcf  24100  fclscf  24143  ufilcmp  24150  cnpfcf  24159  cnextfun  24182  tgpmulg  24211  symgtgp  24224  tgpt0  24237  qustgplem  24239  ustex2sym  24335  ustex3sym  24336  trust  24347  restutop  24355  restutopopn  24356  ustuqtop4  24362  utop3cls  24369  utopreg  24370  cstucnd  24401  ucncn  24402  trcfilu  24411  neipcfilu  24413  ismet2  24451  metequiv2  24628  metcnp  24659  metcnp2  24660  metcnpi3  24664  txmetcnp  24665  metustto  24671  metustsym  24673  metust  24676  cfilucfil  24677  metuel2  24683  psmetutop  24685  restmetu  24688  metucn  24689  ngptgp  24754  tngngp  24772  nmoleub  24849  icccmp  24944  reconnlem2  24946  reconn  24947  xmetdcn2  24956  metdseq0  24973  metdscn  24975  elcncf2  25010  cncfmet  25029  cnheibor  25075  nmoleub2lem2  25236  nmoleub3  25239  cvsi  25250  iscfil2  25386  iscfil3  25393  cfilfcls  25394  equivcfil  25419  caubl  25428  bcthlem5  25448  pmltpc  25570  ovollb2  25609  ovoliunnul  25627  ovolicc2lem4  25640  volsup  25676  ioorf  25693  dyadss  25714  dyaddisjlem  25715  mbfposr  25772  cncombf  25778  mbflimsup  25786  i1fmulclem  25822  mbfi1fseqlem4  25838  iblss2  25926  ellimc2  25997  ellimc3  25999  dvnadd  26049  dvmptfsum  26095  dvferm1  26105  dvferm2  26107  fta1g  26288  plyeq0lem  26328  plydivex  26419  fta1  26430  aalioulem2  26455  aalioulem3  26456  ulmuni  26513  ulmbdd  26519  ulmdvlem3  26523  mtest  26525  abelthlem8  26560  efopn  26781  cxpmul2z  26814  cxpcn3lem  26870  jensen  27111  lgambdd  27159  lgamucov  27160  isppw2  27237  mersenne  27349  dchrelbas3  27360  dchrptlem1  27386  dchrpt  27389  lgsval2lem  27429  lgsdchrval  27476  lgsquad3  27509  2sqb  27554  2sqmo  27559  pntrsumbnd2  27689  pntpbnd  27710  pntibnd  27715  nosupno  27825  noinfno  27840  noetasuplem4  27858  noetalem1  27863  madebday  28051  cofcutr  28075  negsprop  28186  mulscom  28290  absmuls  28395  addonbday  28430  bdayfinbndlem1  28618  z12sge0  28634  remulscl  28653  tgjustr  28701  tglowdim1i  28728  tgbtwndiff  28733  tgifscgr  28735  iscgrglt  28741  tgcgrxfr  28745  lnext  28794  tgbtwnconn1lem3  28801  tgbtwnconn1  28802  legval  28811  legov  28812  legov2  28813  legtrd  28816  legtri3  28817  legso  28826  hlcgrex  28843  hlcgreu  28845  tglnne  28855  tglndim0  28856  tglineeltr  28858  tglinethru  28863  tglinesseq  28867  tglnne0  28868  colline  28877  tglowdim2l  28878  tglowdim2ln  28879  tglnpt2  28880  tglnpt3  28881  tglnpt4  28882  mirreu3  28885  miriso  28901  midexlem  28923  isperp  28943  perpcom  28944  perpneq  28945  isperp2  28946  footexALT  28949  footex  28952  colperpexlem3  28963  opphllem  28966  midex  28968  oppne3  28974  opptgdim2  28976  opphllem2  28979  opphllem3  28980  opphllem5  28982  opphllem6  28983  opphl  28985  outpasch  28986  lnopp2hpgb  28994  colopp  29000  plngrnssp  29009  lnincplng  29014  plngrotlem1  29017  plngrotlem3  29019  lnssplng  29022  plng3p  29023  lmieu  29036  trgcopy  29056  trgcopyeu  29058  iscgra1  29062  cgrane1  29064  cgrane2  29065  cgrane3  29066  cgrahl1  29068  cgrahl2  29069  cgracgr  29070  cgraswap  29072  cgracom  29074  cgratr  29075  flatcgra  29076  cgrabtwn  29078  cgrahl  29079  dfcgra2  29082  sacgr  29083  acopyeu  29086  inaghl  29097  cgrg3col4  29105  f1otrg  29129  f1otrge  29130  axsegcon  29186  axeuclidlem  29221  upgr1eopALT  29376  usgr1eop  29509  pthdepisspth  29993  wpthswwlks2on  30222  clwwlkf1  30309  clwwlknscsh  30322  2pthfrgr  30544  n4cyclfrgr  30551  frgrwopreglem5  30581  frgrwopreglem5ALT  30582  friendshipgt3  30658  smcnlem  30958  0lno  31051  ubthlem1  31131  ubthlem3  31133  chocunii  31562  occl  31565  5oalem1  31915  3oalem2  31924  nmopub2tALT  32170  nmfnleub2  32187  lnconi  32294  kbass5  32381  mdslmd1lem1  32586  mdslmd1lem2  32587  cdj1i  32694  opreu2reuALT  32733  disjabrex  32837  disjabrexf  32838  2ndresdju  32906  acunirnmpt  32916  acunirnmpt2  32917  acunirnmpt2f  32918  aciunf1lem  32919  fnpreimac  32927  fgreu  32928  suppovss  32938  xrge0infss  33017  xrofsup  33024  elq2  33069  fsumiunle  33086  2exple2exp  33091  s3f1  33180  ccatf1  33182  ccatws1f1o  33184  swrdf1  33189  ressprs  33199  dfmgc2  33229  mgcf1o  33236  xrge0addgt0  33250  mndlrinvb  33258  mndlactf1  33259  mndlactfo  33260  mndractf1  33261  mndractfo  33262  mndlactf1o  33263  gsumfs2d  33294  suppgsumssiun  33305  gsumwun  33309  gsumwrd2dccatlem  33310  psgnfzto1stlem  33333  fzto1st1  33335  cycpmco2  33366  cycpmrn  33376  cyc3genpm  33385  cycpmconjs  33389  cyc3conja  33390  conjga  33403  fxpsubrg  33407  submarchi  33419  isarchi3  33420  archiabllem1  33426  archiabllem2a  33427  isarchiofld  33432  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnlem4  33478  elrgspnsubrunlem2  33481  erler  33498  rlocaddval  33502  rlocmulval  33503  rloccring  33504  rloc1r  33506  rlocisunit  33509  subrdom  33518  ricdomn1  33522  isdrng4  33531  fracfld  33544  imaslmod  33588  dvdsruasso  33614  unitprodclb  33618  nsgqusf1olem2  33639  lmhmqusker  33642  intlidl  33644  rhmquskerlem  33649  elrspunidl  33652  elrspunsn  33653  rhmimaidl  33656  mxidlprm  33670  ssmxidl  33674  opprqusplusg  33688  opprqusmulr  33690  qsdrngilem  33693  qsdrngi  33694  drnglring  33699  dflring2  33700  dflringlem2  33702  rsprprmprmidl  33729  rsprprmprmidlb  33730  rprmirred  33738  rprmirredb  33739  rprmdvdspow  33740  rprmdvdsprod  33741  1arithidom  33744  1arithufdlem2  33752  1arithufdlem3  33753  1arithufdlem4  33754  dfufd2lem  33756  dfufd2  33757  zringfrac  33761  deg1prod  33790  ply1dg3rt0irred  33791  r1plmhm  33816  r1pquslmic  33817  0mplrim  33821  mplidomlem  33834  extvfvcl  33843  mplmulmvr  33846  mplvrpmga  33852  psrgsum  33855  psrmonprod  33859  esplyfval3  33879  esplyfval1  33880  esplyfvaln  33881  esplyind  33882  exsslsb  33904  lindsunlem  33931  lindsun  33932  dimkerim  33934  fedgmullem1  33936  fedgmul  33938  dimlssid  33939  evls1fldgencl  33977  fldextrspunlsplem  33980  extdgfialg  34001  minplyirred  34018  fldext2chn  34035  constrmon  34051  constrconj  34052  constrfin  34053  constrelextdg2  34054  constrextdg2lem  34055  constrextdg2  34056  constrext2chnlem  34057  constrfiss  34058  cos9thpiminplylem2  34090  mdetpmtr1  34130  txomap  34141  qtophaus  34143  cmpcref  34157  zarclsun  34177  zarclssn  34180  zarcmplem  34188  pstmxmet  34204  sqsscirc1  34215  ordtrest2NEWlem  34229  ordtconnlem1  34231  pnfneige0  34258  lmxrge0  34259  lmdvg  34260  qqhval2  34289  esumcst  34370  esumrnmpt2  34375  esumfsup  34377  esumcvg  34393  esum2d  34400  esumiun  34401  sigaclfu2  34428  insiga  34444  ldsysgenld  34467  ldgenpisyslem1  34470  fiunelros  34481  measinb  34528  imambfm  34569  oms0  34604  omssubadd  34607  carsgclctunlem3  34627  eulerpartlemgvv  34683  dstrvprob  34779  signstfvneq0  34876  actfunsnrndisj  34909  reprinfz1  34926  breprexp  34937  afsval  34978  derangenlem  35534  sconnpi1  35602  cvmsss2  35637  cvmopnlem  35641  cvmlift3lem7  35688  msrval  35901  ifscgr  36407  cgrxfr  36418  btwnconn1lem13  36462  outsideofeu  36494  nmulcom  36557  neibastop2lem  36733  weiunso  36839  irrdifflemf  37829  irrdiff  37830  matunitlindflem1  38127  matunitlindflem2  38128  poimirlem14  38145  poimirlem22  38153  poimirlem29  38160  broucube  38165  heicant  38166  mblfinlem1  38168  itg2addnclem  38182  ftc1cnnc  38203  ftc1anclem7  38210  sstotbnd2  38285  equivtotbnd  38289  isbnd3  38295  ssbnd  38299  totbndbnd  38300  cntotbnd  38307  heibor1lem  38320  rrncmslem  38343  lssats  39648  lsat0cv  39669  lkrlss  39731  lfl1dim  39757  lfl1dim2N  39758  lkrpssN  39799  hlhgt2  40025  3dim2  40104  2dim  40106  lplncvrlvol  40252  paddasslem11  40466  pmapjat1  40489  2polssN  40551  pclfinclN  40586  pexmidlem8N  40613  lhpexle1lem  40643  4atex  40712  ltrnid  40771  trlator0  40807  cdlemg2cex  41227  tendodi1  41420  tendodi2  41421  diblss  41806  dihopelvalcpre  41884  dihatexv  41974  mapdval4N  42268  fldhmf1  42719  mndmolinv  42724  primrootscoprmpow  42728  posbezout  42729  primrootscoprbij2  42732  primrootspoweq0  42735  aks6d1c2p2  42748  hashscontpow  42751  aks6d1c2lem4  42756  aks6d1c2  42759  aks6d1c5  42768  sticksstones8  42782  sticksstones12  42787  sticksstones22  42797  aks6d1c6lem3  42801  aks6d1c6isolem1  42803  unitscyglem3  42826  aks5  42833  sn-subeu  43048  sn-0tie0  43085  fiabv  43166  frlmsnic  43170  fsuppind  43184  prjspersym  43201  dffltz  43228  nna4b4nsq  43254  mzpindd  43339  mzpsubst  43341  mzpcompact2lem  43344  eldioph2b  43356  irrapxlem3  43413  irrapxlem5  43415  pellex  43424  pell1234qrdich  43450  pell14qrexpcl  43456  congabseq  43563  jm2.26a  43589  jm2.26lem3  43590  rmydioph  43603  lnrfg  43708  hbt  43719  cantnftermord  43909  cantnfresb  43913  cantnf2  43914  oawordex2  43915  omabs2  43921  tfsconcatfv  43930  tfsconcatrev  43937  ofoaass  43949  nadd2rabtr  43973  nadd1suc  43981  naddgeoa  43983  rfovcnvf1od  44592  clsk3nimkb  44628  ntrneiiso  44679  ntrneikb  44682  ntrneixb  44683  ntrneik3  44684  ntrneix3  44685  ntrneik13  44686  ntrneix13  44687  4an4132  45073  iunconnlem2  45508  modelaxrep  45555  fnchoice  45607  cncmpmax  45610  ssinc  45663  ssdec  45664  disjf1  45759  supxrge  45912  suplesup  45913  infxr  45940  infleinf  45945  unb2ltle  45987  rexabslelem  45990  uzub  46003  supminfxr  46036  climrec  46177  climsuse  46182  islptre  46193  addlimc  46220  0ellimcdiv  46221  limsuppnfdlem  46273  limsupub  46276  limsuppnflem  46282  limsupubuz  46285  climinf3  46288  limsupmnflem  46292  climxrre  46322  liminfreuzlem  46374  liminflimsupclim  46379  xlimliminflimsup  46434  icccncfext  46459  cncfiooicclem1  46465  fperdvper  46491  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvmptfprodlem  46516  dvmptfprod  46517  dvnprodlem2  46519  stoweidlem7  46579  stoweidlem34  46606  stoweidlem52  46624  stoweidlem60  46632  wallispilem3  46639  fourierdlem34  46713  fourierdlem38  46717  fourierdlem39  46718  fourierdlem48  46726  fourierdlem50  46728  fourierdlem51  46729  fourierdlem73  46751  fourierdlem76  46754  fourierdlem77  46755  fourierdlem80  46758  fourierdlem87  46765  fourierdlem103  46781  fourierdlem104  46782  etransclem32  46838  etransclem33  46839  sge0f1o  46954  sge0pr  46966  sge0isum  46999  iundjiun  47032  meaiininclem  47058  hoicvr  47120  pimdecfgtioo  47289  pimincfltioo  47290  preimageiingt  47292  preimaleiinlt  47293  smflimlem2  47344  smflimlem4  47346  smfmullem3  47365  smflimmpt  47382  smfinflem  47389  smfpimne2  47412  fsupdm  47414  finfdm  47418  cfsetsnfsetfo  47652  funressnbrafv2  47836  imasetpreimafvbijlemf1  48008  bgoldbtbndlem2  48426  bgoldbtbndlem3  48427  bgoldbtbnd  48429  isuspgrim  48516  stgrusgra  48579  isubgr3stgrlem6  48591  2zlidl  48860  lindslinindsimp2  49094  snlindsntor  49102  lincresunit2  49109  islindeps2  49114  imaf1co  49784  imasubc3  49785  fucofvalg  49947  fuco21  49965  precofvalALT  49997  lanfval  50242  ranfval  50243