Theorem simpllr 763

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 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad3antlr 718	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  fsnex  6858  soisoi  6898  f1o2ndf1  7616  tz7.49  7877  omabs  8066  omxpenlem  8406  fopwdom  8413  findcard3  8548  frfi  8550  finsschain  8618  marypha1lem  8684  wdomtr  8826  cantnfp1  8930  harcard  9193  numacn  9261  infunsdom1  9425  sornom  9489  ssfin4  9522  fin1a2lem11  9622  fin1a2lem13  9624  fpwwe2lem13  9854  pwfseq  9876  mulcmpblnr  10283  00id  10607  addid1  10612  cnegex  10613  negeu  10668  add20  10945  ltmul12a  11289  lediv12a  11326  fiminreOLD  11383  cru  11423  qextltlem  12405  xleadd1a  12455  xmullem  12466  xlemul1a  12490  ixxss12  12567  ioodisj  12677  fsuppmapnn0fz  13172  seqf1o  13219  mulexpz  13277  leexp1a  13347  faclbnd  13458  swrdswrdlem  13876  abs3lem  14549  rexico  14564  cau3lem  14565  rlim3  14706  ello12  14724  lo1bdd2  14732  elo12  14735  rlimconst  14752  isercoll  14875  climcau  14878  climbdd  14879  summolem2  14923  fsumconst  14995  o1fsum  15018  incexclem  15041  fprodconst  15182  bitsfzo  15634  dvdsmulgcd  15751  pc2dvds  16061  pcz  16063  pcadd  16071  pcfac  16081  vdwmc2  16161  vdwlem2  16164  vdwlem10  16172  vdw  16176  ramcl  16211  sbcie3s  16387  firest  16552  prdsval  16574  mreexd  16761  mreexexlemd  16763  iscat  16791  cidfval  16795  iscatd2  16800  catcocl  16804  catass  16805  catpropd  16827  cidpropd  16828  moni  16854  monpropd  16855  issubc  16953  subccocl  16963  funcco  16989  funcpropd  17018  fullpropd  17038  nati  17073  natpropd  17094  fucpropd  17095  xpcpropd  17306  curfuncf  17336  curf2ndf  17345  yonffthlem  17380  acsfiindd  17635  mndpropd  17774  mhmeql  17822  isgrpinv  17933  dfgrp3lem  17974  mhmmnd  17998  conjnmzb  18154  gass  18192  symgextf  18296  dfod2  18442  gexdvds  18460  sylow3lem2  18504  efgredlem  18622  efgredlemOLD  18623  efgredeu  18628  ghmcmn  18700  oddvdssubg  18721  dprdfcntz  18877  pgpfaclem3  18945  issrg  18970  isring  19014  dvdsrmul1  19116  issubdrg  19273  islmhm2  19522  lmhmeql  19539  lssacsex  19628  issubassa2  19829  opsrval  19958  isphl  20464  uvcf1  20628  lindfmm  20663  scmatmats  20814  smatvscl  20827  mdetunilem7  20921  gsummatr01lem4  20961  m2cpmfo  21058  pmatcollpw3fi1lem1  21088  pm2mpf1lem  21096  pm2mpf1  21101  mp2pm2mplem4  21111  pm2mpghm  21118  chfacfscmulfsupp  21161  chfacfpmmulfsupp  21165  cctop  21308  neiptoptop  21433  neiptopreu  21435  tgrest  21461  ordtrest2lem  21505  cnss1  21578  cncnp  21582  isnrm3  21661  uncmp  21705  cmpfi  21710  iunconn  21730  1stcrest  21755  subislly  21783  islly2  21786  cldllycmp  21797  lly1stc  21798  llycmpkgen2  21852  kgencn  21858  xkoccn  21921  ptcnplem  21923  pthaus  21940  txhaus  21949  txkgen  21954  xkohaus  21955  xkococnlem  21961  txconn  21991  regr1lem2  22042  kqreglem1  22043  reghmph  22095  nrmhmph  22096  trfil2  22189  ufileu  22221  flimopn  22277  flimcf  22284  fclscf  22327  ufilcmp  22334  cnpfcf  22343  cnextfun  22366  tgpmulg  22395  symgtgp  22403  tgpt0  22420  qustgplem  22422  ustex2sym  22518  ustex3sym  22519  trust  22531  restutop  22539  restutopopn  22540  ustuqtop4  22546  utop3cls  22553  utopreg  22554  cstucnd  22586  ucncn  22587  trcfilu  22596  neipcfilu  22598  ismet2  22636  metequiv2  22813  metcnp  22844  metcnp2  22845  metcnpi3  22849  txmetcnp  22850  metustto  22856  metustsym  22858  metust  22861  cfilucfil  22862  metuel2  22868  psmetutop  22870  restmetu  22873  metucn  22874  ngptgp  22938  tngngp  22956  nmoleub  23033  icccmp  23126  reconnlem2  23128  reconn  23129  xmetdcn2  23138  metdseq0  23155  metdscn  23157  elcncf2  23191  cncfmet  23209  cnheibor  23252  nmoleub2lem2  23413  nmoleub3  23416  cvsi  23427  iscfil2  23562  iscfil3  23569  cfilfcls  23570  equivcfil  23595  caubl  23604  bcthlem5  23624  pmltpc  23744  ovollb2  23783  ovoliunnul  23801  ovolicc2lem4  23814  volsup  23850  ioorf  23867  dyadss  23888  dyaddisjlem  23889  mbfposr  23946  cncombf  23952  mbflimsup  23960  i1fmulclem  23996  mbfi1fseqlem4  24012  iblss2  24099  ellimc2  24168  ellimc3  24170  dvnadd  24219  dvmptfsum  24265  dvferm1  24275  dvferm2  24277  fta1g  24454  plyeq0lem  24493  plydivex  24579  fta1  24590  aalioulem2  24615  aalioulem3  24616  ulmuni  24673  ulmbdd  24679  ulmdvlem3  24683  mtest  24685  abelthlem8  24720  efopn  24932  cxpmul2z  24965  cxpcn3lem  25019  jensen  25258  lgambdd  25306  lgamucov  25307  isppw2  25384  mersenne  25495  dchrelbas3  25506  dchrptlem1  25532  dchrpt  25535  lgsval2lem  25575  lgsdchrval  25622  lgsquad3  25655  2sqb  25700  2sqmo  25705  pntrsumbnd2  25835  pntpbnd  25856  pntibnd  25861  istrkgc  25932  istrkgb  25933  tgjustr  25952  tglowdim1i  25979  tgbtwndiff  25984  tgifscgr  25986  iscgrglt  25992  tgcgrxfr  25996  lnext  26045  tgbtwnconn1lem3  26052  tgbtwnconn1  26053  legval  26062  legov  26063  legov2  26064  legtrd  26067  legtri3  26068  legso  26077  hlcgrex  26094  hlcgreu  26096  tglnne  26106  tglndim0  26107  tglineeltr  26109  tglinethru  26114  tglnne0  26118  tglnpt2  26119  colline  26127  tglowdim2l  26128  tglowdim2ln  26129  mirreu3  26132  miriso  26148  midexlem  26170  isperp  26190  perpcom  26191  perpneq  26192  isperp2  26193  footexALT  26196  footex  26199  colperpexlem3  26210  opphllem  26213  midex  26215  oppne3  26221  opptgdim2  26223  opphllem2  26226  opphllem3  26227  opphllem5  26229  opphllem6  26230  opphl  26232  outpasch  26233  lnopp2hpgb  26241  colopp  26247  lmieu  26262  trgcopy  26282  trgcopyeu  26284  iscgra1  26288  cgrane1  26290  cgrane2  26291  cgrane3  26292  cgrahl1  26294  cgrahl2  26295  cgracgr  26296  cgraswap  26298  cgracom  26300  cgratr  26301  flatcgra  26302  cgrabtwn  26304  cgrahl  26305  dfcgra2  26308  sacgr  26309  sacgrOLD  26310  acopyeu  26313  inaghl  26324  cgrg3col4  26332  f1otrg  26350  f1otrge  26351  axsegcon  26406  axeuclidlem  26441  upgr1eopALT  26595  usgr1eop  26725  pthdepisspth  27214  wpthswwlks2on  27457  clwwlkf1OLD  27556  clwwlkf1  27561  clwwlknscsh  27576  2pthfrgr  27808  n4cyclfrgr  27815  frgrwopreglem5  27845  frgrwopreglem5ALT  27846  friendshipgt3  27945  smcnlem  28241  0lno  28334  ubthlem1  28415  ubthlem3  28417  chocunii  28849  occl  28852  5oalem1  29202  3oalem2  29211  nmopub2tALT  29457  nmfnleub2  29474  lnconi  29581  kbass5  29668  mdslmd1lem1  29873  mdslmd1lem2  29874  cdj1i  29981  opreu2reuALT  30012  disjabrex  30088  disjabrexf  30089  acunirnmpt  30156  acunirnmpt2  30157  acunirnmpt2f  30158  aciunf1lem  30159  fnpreimac  30168  fgreu  30169  suppovss  30176  xrge0infss  30225  xrofsup  30233  fsumiunle  30280  ressprs  30352  xrge0addgt0  30388  submarchi  30437  isarchi3  30438  archiabllem1  30444  archiabllem2a  30445  gsumle  30478  suborng  30523  isarchiofld  30525  imaslmod  30557  lindsunlem  30605  lindsun  30606  dimkerim  30608  fedgmullem1  30610  fedgmul  30612  psgnfzto1stlem  30648  fzto1st1  30650  mdetpmtr1  30687  fimaproj  30698  txomap  30699  qtophaus  30701  cmpcref  30715  pstmxmet  30738  sqsscirc1  30752  ordtrest2NEWlem  30766  ordtconnlem1  30768  pnfneige0  30795  lmxrge0  30796  lmdvg  30797  qqhval2  30824  esumcst  30923  esumrnmpt2  30928  esumfsup  30930  esumcvg  30946  esum2d  30953  esumiun  30954  sigaclfu2  30982  insiga  30998  ldsysgenld  31021  ldgenpisyslem1  31024  fiunelros  31035  measinb  31082  imambfm  31122  oms0  31157  omssubadd  31160  carsgclctunlem3  31180  eulerpartlemgvv  31236  dstrvprob  31332  sgnsub  31405  signstfvneq0  31450  actfunsnrndisj  31485  reprinfz1  31502  breprexp  31513  afsval  31551  derangenlem  31963  sconnpi1  32031  cvmsss2  32066  cvmopnlem  32070  cvmlift3lem7  32117  msrval  32245  frpomin  32539  fprlem2  32599  frrlem16  32604  nosupno  32664  noetalem3  32680  noetalem5  32682  ifscgr  32966  cgrxfr  32977  btwnconn1lem13  33021  outsideofeu  33053  neibastop2lem  33169  matunitlindflem1  34277  matunitlindflem2  34278  poimirlem14  34295  poimirlem22  34303  poimirlem29  34310  broucube  34315  heicant  34316  mblfinlem1  34318  itg2addnclem  34332  ftc1cnnc  34355  ftc1anclem7  34362  sstotbnd2  34442  equivtotbnd  34446  isbnd3  34452  ssbnd  34456  totbndbnd  34457  cntotbnd  34464  heibor1lem  34477  rrncmslem  34500  lssats  35541  lsat0cv  35562  lkrlss  35624  lfl1dim  35650  lfl1dim2N  35651  lkrpssN  35692  hlhgt2  35918  3dim2  35997  2dim  35999  lplncvrlvol  36145  paddasslem11  36359  pmapjat1  36382  2polssN  36444  pclfinclN  36479  pexmidlem8N  36506  lhpexle1lem  36536  4atex  36605  ltrnid  36664  trlator0  36700  cdlemg2cex  37120  tendodi1  37313  tendodi2  37314  diblss  37699  dihopelvalcpre  37777  dihatexv  37867  mapdval4N  38161  frlmsnic  38531  prjspersym  38609  dffltz  38623  mzpindd  38683  mzpsubst  38685  mzpcompact2lem  38688  eldioph2b  38700  irrapxlem3  38762  irrapxlem5  38764  pellex  38773  pell1234qrdich  38799  pell14qrexpcl  38805  congabseq  38912  jm2.26a  38938  jm2.26lem3  38939  rmydioph  38952  lnrfg  39060  hbt  39071  rfovcnvf1od  39658  clsk3nimkb  39698  ntrneiiso  39749  ntrneikb  39752  ntrneixb  39753  ntrneik3  39754  ntrneix3  39755  ntrneik13  39756  ntrneix13  39757  4an4132  40196  iunconnlem2  40632  fnchoice  40649  cncmpmax  40652  ssinc  40720  ssdec  40721  disjf1  40813  supxrge  40981  suplesup  40982  infxr  41010  infleinf  41015  unb2ltle  41066  rexabslelem  41069  uzub  41082  supminfxr  41117  climrec  41261  climsuse  41266  islptre  41277  addlimc  41306  0ellimcdiv  41307  limsuppnfdlem  41359  limsupub  41362  limsuppnflem  41368  limsupubuz  41371  climinf3  41374  limsupmnflem  41378  climxrre  41408  liminfreuzlem  41460  liminflimsupclim  41465  xlimliminflimsup  41520  icccncfext  41546  cncfiooicclem1  41552  fperdvper  41579  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  dvmptfprodlem  41605  dvmptfprod  41606  dvnprodlem2  41608  stoweidlem7  41669  stoweidlem34  41696  stoweidlem52  41714  stoweidlem60  41722  wallispilem3  41729  fourierdlem34  41803  fourierdlem38  41807  fourierdlem39  41808  fourierdlem48  41816  fourierdlem50  41818  fourierdlem51  41819  fourierdlem73  41841  fourierdlem76  41844  fourierdlem77  41845  fourierdlem80  41848  fourierdlem87  41855  fourierdlem103  41871  fourierdlem104  41872  etransclem32  41928  etransclem33  41929  sge0f1o  42041  sge0pr  42053  sge0isum  42086  iundjiun  42119  meaiininclem  42145  pimdecfgtioo  42372  pimincfltioo  42373  preimageiingt  42375  preimaleiinlt  42376  smflimlem2  42425  smflimlem4  42427  smfmullem3  42445  smflimmpt  42461  smfinflem  42468  funressnbrafv2  42795  bgoldbtbndlem2  43279  bgoldbtbndlem3  43280  bgoldbtbnd  43282  isomuspgrlem2  43306  mgmhmeql  43378  isrng  43451  2zlidl  43509  lindslinindsimp2  43825  snlindsntor  43833  lincresunit2  43840  islindeps2  43845