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  6343  fsnex  7283  soisoi  7328  f1o2ndf1  8118  fimaproj  8132  fprlem2  8299  tz7.49  8433  omabs  8638  cofon1  8659  naddssim  8673  omxpenlem  9067  fopwdom  9074  findcard3  9244  frfi  9246  finsschain  9317  marypha1lem  9394  wemappo  9512  wdomtr  9538  cantnfp1  9651  ttrcltr  9686  harcard  9965  numacn  10034  infunsdom1  10196  sornom  10262  ssfin4  10295  fin1a2lem11  10395  fin1a2lem13  10397  fpwwe2lem12  10628  pwfseq  10650  mulcmpblnr  11057  00id  11386  addrid  11391  cnegex  11392  negeu  11448  add20  11727  ltmul12a  12072  lediv12a  12109  cru  12211  qextltlem  13229  xleadd1a  13280  xmullem  13291  xlemul1a  13315  ixxss12  13393  ioodisj  13510  fvf1tp  13824  fsuppmapnn0fz  14034  seqf1o  14081  mulexpz  14140  leexp1a  14213  faclbnd  14328  swrdswrdlem  14743  sgnsub  15145  abs3lem  15392  rexico  15407  cau3lem  15408  rlim3  15551  ello12  15569  lo1bdd2  15577  elo12  15580  rlimconst  15597  isercoll  15721  climcau  15724  climbdd  15725  summolem2  15769  fsumconst  15843  o1fsum  15867  incexclem  15892  fprodconst  16034  bitsfzo  16494  dvdsmulgcd  16615  pc2dvds  16940  pcz  16942  pcadd  16950  pcfac  16960  vdwmc2  17040  vdwlem2  17043  vdwlem10  17051  vdw  17055  ramcl  17090  sbcie3s  17223  firest  17486  prdsval  17509  mreexd  17699  mreexexlemd  17701  iscat  17729  cidfval  17733  iscatd2  17738  catcocl  17742  catass  17743  catpropd  17766  cidpropd  17767  moni  17794  monpropd  17795  issubc  17893  subccocl  17903  funcco  17929  funcpropd  17960  fullpropd  17980  nati  18016  natpropd  18037  fucpropd  18038  xpcpropd  18265  curfuncf  18295  curf2ndf  18304  yonffthlem  18339  acsfiindd  18610  chnind  18678  chnso  18681  mgmhmeql  18775  sgrppropd  18790  mndpropd  18818  mhmeql  18886  smndex1mgm  18970  isgrpinv  19061  dfgrp3lem  19105  mhmmnd  19131  cycsubm  19274  cycsubmcom  19276  conjnmzb  19324  ghmqusnsg  19353  ghmquskerlem3  19357  ghmqusker  19358  gass  19372  symgextf  19488  dfod2  19635  gexdvds  19655  sylow3lem2  19699  efgredlem  19818  efgredeu  19823  ghmcmn  19902  oddvdssubg  19926  dprdfcntz  20088  pgpfaclem3  20156  gsumle  20216  isrng  20233  issrg  20271  isring  20320  dvdsrmul1  20452  isdrng4  20826  issubdrg  20864  suborng  20960  islmhm2  21140  lmhmeql  21157  lssacsex  21249  rhmpreimaidl  21397  rhmqusnsg  21406  prmidl2  21447  isprmidlc  21453  rhmpreimaprmidl  21460  qsidomlem2  21462  ssdifidllem  21465  ssdifidlprm  21467  isphl  21759  uvcf1  21923  lindfmm  21958  sraassab  21999  issubassa2  22023  opsrval  22178  psdmul  22310  scmatmats  22649  smatvscl  22662  mdetunilem7  22756  gsummatr01lem4  22796  m2cpmfo  22894  pmatcollpw3fi1lem1  22924  pm2mpf1lem  22932  pm2mpf1  22937  mp2pm2mplem4  22947  pm2mpghm  22954  chfacfscmulfsupp  22997  chfacfpmmulfsupp  23001  cctop  23144  neiptoptop  23269  neiptopreu  23271  tgrest  23297  ordtrest2lem  23341  cnss1  23414  cncnp  23418  isnrm3  23497  uncmp  23541  cmpfi  23546  iunconn  23566  1stcrest  23591  subislly  23619  islly2  23622  cldllycmp  23633  lly1stc  23634  llycmpkgen2  23688  kgencn  23694  xkoccn  23757  ptcnplem  23759  pthaus  23776  txhaus  23785  txkgen  23790  xkohaus  23791  xkococnlem  23797  txconn  23827  regr1lem2  23878  kqreglem1  23879  reghmph  23931  nrmhmph  23932  trfil2  24025  ufileu  24057  flimopn  24113  flimcf  24120  fclscf  24163  ufilcmp  24170  cnpfcf  24179  cnextfun  24202  tgpmulg  24231  symgtgp  24244  tgpt0  24257  qustgplem  24259  ustex2sym  24355  ustex3sym  24356  trust  24367  restutop  24375  restutopopn  24376  ustuqtop4  24382  utop3cls  24389  utopreg  24390  cstucnd  24421  ucncn  24422  trcfilu  24431  neipcfilu  24433  ismet2  24471  metequiv2  24648  metcnp  24679  metcnp2  24680  metcnpi3  24684  txmetcnp  24685  metustto  24691  metustsym  24693  metust  24696  cfilucfil  24697  metuel2  24703  psmetutop  24705  restmetu  24708  metucn  24709  ngptgp  24774  tngngp  24792  nmoleub  24869  icccmp  24964  reconnlem2  24966  reconn  24967  xmetdcn2  24976  metdseq0  24993  metdscn  24995  elcncf2  25030  cncfmet  25049  cnheibor  25095  nmoleub2lem2  25256  nmoleub3  25259  cvsi  25270  iscfil2  25406  iscfil3  25413  cfilfcls  25414  equivcfil  25439  caubl  25448  bcthlem5  25468  pmltpc  25590  ovollb2  25629  ovoliunnul  25647  ovolicc2lem4  25660  volsup  25696  ioorf  25713  dyadss  25734  dyaddisjlem  25735  mbfposr  25792  cncombf  25798  mbflimsup  25806  i1fmulclem  25842  mbfi1fseqlem4  25858  iblss2  25946  ellimc2  26017  ellimc3  26019  dvnadd  26069  dvmptfsum  26115  dvferm1  26125  dvferm2  26127  fta1g  26308  plyeq0lem  26348  plydivex  26439  fta1  26450  aalioulem2  26475  aalioulem3  26476  ulmuni  26533  ulmbdd  26539  ulmdvlem3  26543  mtest  26545  abelthlem8  26580  efopn  26801  cxpmul2z  26834  cxpcn3lem  26890  jensen  27131  lgambdd  27179  lgamucov  27180  isppw2  27257  mersenne  27369  dchrelbas3  27380  dchrptlem1  27406  dchrpt  27409  lgsval2lem  27449  lgsdchrval  27496  lgsquad3  27529  2sqb  27574  2sqmo  27579  pntrsumbnd2  27709  pntpbnd  27730  pntibnd  27735  nosupno  27845  noinfno  27860  noetasuplem4  27878  noetalem1  27883  madebday  28071  cofcutr  28095  negsprop  28206  mulscom  28310  absmuls  28415  addonbday  28450  bdayfinbndlem1  28638  z12sge0  28654  remulscl  28673  tgjustr  28721  tglowdim1i  28748  tgbtwndiff  28753  tgifscgr  28755  iscgrglt  28761  tgcgrxfr  28765  lnext  28814  tgbtwnconn1lem3  28821  tgbtwnconn1  28822  legval  28831  legov  28832  legov2  28833  legtrd  28836  legtri3  28837  legso  28846  hlcgrex  28866  hlcgreu  28868  tglnne  28879  tglndim0  28880  tglineeltr  28882  tglinethru  28887  tglinesseq  28891  tglnne0  28892  colline  28901  tglowdim2l  28902  tglowdim2ln  28903  tglnpt2  28904  tglnpt3  28905  tglnpt4  28906  mirreu3  28909  miriso  28925  midexlem  28947  isperp  28970  perpcom  28971  perpneq  28972  isperp2  28973  footexALT  28976  footex  28979  colperpexlem3  28991  opphllem  28994  midex  28996  oppne3  29002  opptgdim2  29004  opphllem2  29007  opphllem3  29008  opphllem5  29010  opphllem6  29011  opphl  29013  outpasch  29015  lnopp2hpgb  29023  colopp  29029  plngrnssp  29039  lnincplng  29044  plngrotlem1  29047  plngrotlem3  29049  lnssplng  29052  plng3p  29057  lmieu  29071  trgcopy  29093  trgcopyeu  29095  iscgra1  29099  cgrane1  29101  cgrane2  29102  cgrane3  29103  cgrahl1  29105  cgrahl2  29106  cgracgr  29107  cgraswap  29109  cgracom  29111  cgratr  29112  flatcgra  29113  cgrabtwn  29115  cgrahl  29116  dfcgra2  29119  sacgr  29120  acopyeu  29123  ragcgra  29124  cgrarag  29125  ragsupplcgra  29126  inaghl  29140  cgrg3col4  29148  prlnghpg  29174  dfprlng2  29175  dfprlng3  29176  perpprlng  29178  prlngex  29179  prlngmolem1  29180  prlngmolem2  29181  prlngmo2  29184  prlngplngtr  29187  quadcgrprlng  29194  f1otrg  29198  f1otrge  29199  axsegcon  29255  axeuclidlem  29290  upgr1eopALT  29445  usgr1eop  29578  pthdepisspth  30062  wpthswwlks2on  30291  clwwlkf1  30378  clwwlknscsh  30391  2pthfrgr  30613  n4cyclfrgr  30620  frgrwopreglem5  30650  frgrwopreglem5ALT  30651  friendshipgt3  30727  smcnlem  31027  0lno  31120  ubthlem1  31200  ubthlem3  31202  chocunii  31631  occl  31634  5oalem1  31984  3oalem2  31993  nmopub2tALT  32239  nmfnleub2  32256  lnconi  32363  kbass5  32450  mdslmd1lem1  32655  mdslmd1lem2  32656  cdj1i  32763  opreu2reuALT  32801  disjabrex  32905  disjabrexf  32906  2ndresdju  32972  acunirnmpt  32982  acunirnmpt2  32983  acunirnmpt2f  32984  aciunf1lem  32985  fnpreimac  32993  fgreu  32994  suppovss  33004  xrge0infss  33083  xrofsup  33090  elq2  33134  fsumiunle  33151  2exple2exp  33156  s3f1  33245  ccatf1  33247  ccatws1f1o  33249  swrdf1  33254  ressprs  33264  dfmgc2  33294  mgcf1o  33301  xrge0addgt0  33315  mndlrinvb  33323  mndlactf1  33324  mndlactfo  33325  mndractf1  33326  mndractfo  33327  mndlactf1o  33328  gsumfs2d  33359  suppgsumssiun  33370  gsumwun  33374  gsumwrd2dccatlem  33375  psgnfzto1stlem  33398  fzto1st1  33400  cycpmco2  33431  cycpmrn  33441  cyc3genpm  33450  cycpmconjs  33454  cyc3conja  33455  conjga  33468  fxpsubrg  33472  submarchi  33484  isarchi3  33485  archiabllem1  33491  archiabllem2a  33492  isarchiofld  33497  elrgspnlem1  33540  elrgspnlem2  33541  elrgspnlem4  33543  elrgspnsubrunlem2  33546  erler  33563  rlocaddval  33567  rlocmulval  33568  rloccring  33569  rloc1r  33571  rlocisunit  33574  subrdom  33583  ricdomn1  33587  fracfld  33607  imaslmod  33651  dvdsruasso  33676  unitprodclb  33680  nsgqusf1olem2  33701  lmhmqusker  33704  intlidl  33706  rhmquskerlem  33711  elrspunidl  33714  elrspunsn  33715  rhmimaidl  33718  mxidlprm  33731  ssmxidl  33735  opprqusplusg  33749  opprqusmulr  33751  qsdrngilem  33754  qsdrngi  33755  drnglring  33760  dflring2  33761  dflringlem2  33763  rsprprmprmidl  33790  rsprprmprmidlb  33791  rprmirred  33799  rprmirredb  33800  rprmdvdspow  33801  rprmdvdsprod  33802  1arithidom  33805  1arithufdlem2  33813  1arithufdlem3  33814  1arithufdlem4  33815  dfufd2lem  33817  dfufd2  33818  zringfrac  33822  deg1prod  33851  ply1dg3rt0irred  33852  r1plmhm  33877  r1pquslmic  33878  0mplrim  33882  mplidomlem  33895  extvfvcl  33904  mplmulmvr  33907  mplvrpmga  33913  psrgsum  33916  psrmonprod  33920  esplyfval3  33940  esplyfval1  33941  esplyfvaln  33942  esplyind  33943  exsslsb  33965  lindsunlem  33992  lindsun  33993  dimkerim  33995  fedgmullem1  33997  fedgmul  33999  dimlssid  34000  evls1fldgencl  34038  fldextrspunlsplem  34041  extdgfialg  34062  minplyirred  34079  fldext2chn  34096  constrmon  34112  constrconj  34113  constrfin  34114  constrelextdg2  34115  constrextdg2lem  34116  constrextdg2  34117  constrext2chnlem  34118  constrfiss  34119  cos9thpiminplylem2  34151  mdetpmtr1  34191  txomap  34202  qtophaus  34204  cmpcref  34218  zarclsun  34238  zarclssn  34241  zarcmplem  34249  pstmxmet  34265  sqsscirc1  34276  ordtrest2NEWlem  34290  ordtconnlem1  34292  pnfneige0  34319  lmxrge0  34320  lmdvg  34321  qqhval2  34350  esumcst  34431  esumrnmpt2  34436  esumfsup  34438  esumcvg  34454  esum2d  34461  esumiun  34462  sigaclfu2  34489  insiga  34505  ldsysgenld  34528  ldgenpisyslem1  34531  fiunelros  34542  measinb  34589  imambfm  34630  oms0  34665  omssubadd  34668  carsgclctunlem3  34688  eulerpartlemgvv  34744  dstrvprob  34840  signstfvneq0  34937  actfunsnrndisj  34970  reprinfz1  34987  breprexp  34998  afsval  35039  derangenlem  35641  sconnpi1  35709  cvmsss2  35744  cvmopnlem  35748  cvmlift3lem7  35795  msrval  36008  ifscgr  36514  cgrxfr  36525  btwnconn1lem13  36569  outsideofeu  36601  nmulcom  36664  nmuladdss  36668  neibastop2lem  36849  weiunso  36955  irrdifflemf  37947  irrdiff  37948  matunitlindflem1  38245  matunitlindflem2  38246  poimirlem14  38263  poimirlem22  38271  poimirlem29  38278  broucube  38283  heicant  38284  mblfinlem1  38286  itg2addnclem  38300  ftc1cnnc  38321  ftc1anclem7  38328  sstotbnd2  38403  equivtotbnd  38407  isbnd3  38413  ssbnd  38417  totbndbnd  38418  cntotbnd  38425  heibor1lem  38438  rrncmslem  38461  lssats  39764  lsat0cv  39785  lkrlss  39847  lfl1dim  39873  lfl1dim2N  39874  lkrpssN  39915  hlhgt2  40141  3dim2  40220  2dim  40222  lplncvrlvol  40368  paddasslem11  40582  pmapjat1  40605  2polssN  40667  pclfinclN  40702  pexmidlem8N  40729  lhpexle1lem  40759  4atex  40828  ltrnid  40887  trlator0  40923  cdlemg2cex  41343  tendodi1  41536  tendodi2  41537  diblss  41922  dihopelvalcpre  42000  dihatexv  42090  mapdval4N  42384  fldhmf1  42835  mndmolinv  42840  primrootscoprmpow  42844  posbezout  42845  primrootscoprbij2  42848  primrootspoweq0  42851  aks6d1c2p2  42864  hashscontpow  42867  aks6d1c2lem4  42872  aks6d1c2  42875  aks6d1c5  42884  sticksstones8  42898  sticksstones12  42903  sticksstones22  42913  aks6d1c6lem3  42917  aks6d1c6isolem1  42919  unitscyglem3  42942  aks5  42949  sn-subeu  43166  sn-0tie0  43203  fiabv  43284  frlmsnic  43288  fsuppind  43302  prjspersym  43319  dffltz  43346  nna4b4nsq  43372  mzpindd  43457  mzpsubst  43459  mzpcompact2lem  43462  eldioph2b  43474  irrapxlem3  43531  irrapxlem5  43533  pellex  43542  pell1234qrdich  43568  pell14qrexpcl  43574  congabseq  43681  jm2.26a  43707  jm2.26lem3  43708  rmydioph  43721  lnrfg  43826  hbt  43837  cantnftermord  44027  cantnfresb  44031  cantnf2  44032  oawordex2  44033  omabs2  44039  tfsconcatfv  44048  tfsconcatrev  44055  ofoaass  44067  nadd2rabtr  44091  nadd1suc  44099  naddgeoa  44101  rfovcnvf1od  44710  clsk3nimkb  44746  ntrneiiso  44797  ntrneikb  44800  ntrneixb  44801  ntrneik3  44802  ntrneix3  44803  ntrneik13  44804  ntrneix13  44805  4an4132  45188  iunconnlem2  45623  modelaxrep  45670  fnchoice  45729  cncmpmax  45732  ssinc  45785  ssdec  45786  disjf1  45881  supxrge  46034  suplesup  46035  infxr  46062  infleinf  46067  unb2ltle  46109  rexabslelem  46112  uzub  46125  supminfxr  46158  climrec  46299  climsuse  46304  islptre  46315  addlimc  46342  0ellimcdiv  46343  limsuppnfdlem  46395  limsupub  46398  limsuppnflem  46404  limsupubuz  46407  climinf3  46410  limsupmnflem  46414  climxrre  46444  liminfreuzlem  46496  liminflimsupclim  46501  xlimliminflimsup  46556  icccncfext  46581  cncfiooicclem1  46587  fperdvper  46613  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  dvmptfprodlem  46638  dvmptfprod  46639  dvnprodlem2  46641  stoweidlem7  46701  stoweidlem34  46728  stoweidlem52  46746  stoweidlem60  46754  wallispilem3  46761  fourierdlem34  46835  fourierdlem38  46839  fourierdlem39  46840  fourierdlem48  46848  fourierdlem50  46850  fourierdlem51  46851  fourierdlem73  46873  fourierdlem76  46876  fourierdlem77  46877  fourierdlem80  46880  fourierdlem87  46887  fourierdlem103  46903  fourierdlem104  46904  etransclem32  46960  etransclem33  46961  sge0f1o  47076  sge0pr  47088  sge0isum  47121  iundjiun  47154  meaiininclem  47180  hoicvr  47242  pimdecfgtioo  47411  pimincfltioo  47412  preimageiingt  47414  preimaleiinlt  47415  smflimlem2  47466  smflimlem4  47468  smfmullem3  47487  smflimmpt  47504  smfinflem  47511  smfpimne2  47534  fsupdm  47536  finfdm  47540  cfsetsnfsetfo  47774  funressnbrafv2  47958  imasetpreimafvbijlemf1  48130  bgoldbtbndlem2  48548  bgoldbtbndlem3  48549  bgoldbtbnd  48551  isuspgrim  48638  stgrusgra  48701  isubgr3stgrlem6  48713  2zlidl  48982  lindslinindsimp2  49220  snlindsntor  49228  lincresunit2  49235  islindeps2  49240  imaf1co  49910  imasubc3  49911  fucofvalg  50073  fuco21  50091  precofvalALT  50123  lanfval  50368  ranfval  50369