Theorem simpllr 776

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 731	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  frpomin  6362  fsnex  7302  soisoi  7347  f1o2ndf1  8145  fimaproj  8158  fprlem2  8324  tz7.49  8483  omabs  8687  cofon1  8708  naddssim  8721  omxpenlem  9111  fopwdom  9118  findcard3  9315  findcard3OLD  9316  frfi  9318  finsschain  9396  marypha1lem  9470  wemappo  9586  wdomtr  9612  cantnfp1  9718  ttrcltr  9753  harcard  10015  numacn  10086  infunsdom1  10249  sornom  10314  ssfin4  10347  fin1a2lem11  10447  fin1a2lem13  10449  fpwwe2lem12  10679  pwfseq  10701  mulcmpblnr  11108  00id  11433  addrid  11438  cnegex  11439  negeu  11495  add20  11772  ltmul12a  12120  lediv12a  12158  cru  12255  qextltlem  13240  xleadd1a  13291  xmullem  13302  xlemul1a  13326  ixxss12  13403  ioodisj  13518  fvf1tp  13825  fsuppmapnn0fz  14033  seqf1o  14080  mulexpz  14139  leexp1a  14211  faclbnd  14325  swrdswrdlem  14738  abs3lem  15373  rexico  15388  cau3lem  15389  rlim3  15530  ello12  15548  lo1bdd2  15556  elo12  15559  rlimconst  15576  isercoll  15700  climcau  15703  climbdd  15704  summolem2  15748  fsumconst  15822  o1fsum  15845  incexclem  15868  fprodconst  16010  bitsfzo  16468  dvdsmulgcd  16589  pc2dvds  16912  pcz  16914  pcadd  16922  pcfac  16932  vdwmc2  17012  vdwlem2  17015  vdwlem10  17023  vdw  17027  ramcl  17062  sbcie3s  17195  firest  17478  prdsval  17501  mreexd  17686  mreexexlemd  17688  iscat  17716  cidfval  17720  iscatd2  17725  catcocl  17729  catass  17730  catpropd  17753  cidpropd  17754  moni  17783  monpropd  17784  issubc  17885  subccocl  17895  funcco  17921  funcpropd  17953  fullpropd  17973  nati  18009  natpropd  18032  fucpropd  18033  xpcpropd  18264  curfuncf  18294  curf2ndf  18303  yonffthlem  18338  acsfiindd  18610  mgmhmeql  18741  sgrppropd  18756  mndpropd  18784  mhmeql  18851  smndex1mgm  18932  isgrpinv  19023  dfgrp3lem  19068  mhmmnd  19094  cycsubm  19232  cycsubmcom  19234  conjnmzb  19283  ghmqusnsg  19312  ghmquskerlem3  19316  ghmqusker  19317  gass  19331  symgextf  19449  dfod2  19596  gexdvds  19616  sylow3lem2  19660  efgredlem  19779  efgredeu  19784  ghmcmn  19863  oddvdssubg  19887  dprdfcntz  20049  pgpfaclem3  20117  isrng  20171  issrg  20205  isring  20254  dvdsrmul1  20385  issubdrg  20797  islmhm2  21054  lmhmeql  21071  lssacsex  21163  rhmpreimaidl  21304  rhmqusnsg  21312  isphl  21663  uvcf1  21829  lindfmm  21864  sraassab  21905  issubassa2  21929  opsrval  22081  psdmul  22187  scmatmats  22532  smatvscl  22545  mdetunilem7  22639  gsummatr01lem4  22679  m2cpmfo  22777  pmatcollpw3fi1lem1  22807  pm2mpf1lem  22815  pm2mpf1  22820  mp2pm2mplem4  22830  pm2mpghm  22837  chfacfscmulfsupp  22880  chfacfpmmulfsupp  22884  cctop  23028  neiptoptop  23154  neiptopreu  23156  tgrest  23182  ordtrest2lem  23226  cnss1  23299  cncnp  23303  isnrm3  23382  uncmp  23426  cmpfi  23431  iunconn  23451  1stcrest  23476  subislly  23504  islly2  23507  cldllycmp  23518  lly1stc  23519  llycmpkgen2  23573  kgencn  23579  xkoccn  23642  ptcnplem  23644  pthaus  23661  txhaus  23670  txkgen  23675  xkohaus  23676  xkococnlem  23682  txconn  23712  regr1lem2  23763  kqreglem1  23764  reghmph  23816  nrmhmph  23817  trfil2  23910  ufileu  23942  flimopn  23998  flimcf  24005  fclscf  24048  ufilcmp  24055  cnpfcf  24064  cnextfun  24087  tgpmulg  24116  symgtgp  24129  tgpt0  24142  qustgplem  24144  ustex2sym  24240  ustex3sym  24241  trust  24253  restutop  24261  restutopopn  24262  ustuqtop4  24268  utop3cls  24275  utopreg  24276  cstucnd  24308  ucncn  24309  trcfilu  24318  neipcfilu  24320  ismet2  24358  metequiv2  24538  metcnp  24569  metcnp2  24570  metcnpi3  24574  txmetcnp  24575  metustto  24581  metustsym  24583  metust  24586  cfilucfil  24587  metuel2  24593  psmetutop  24595  restmetu  24598  metucn  24599  ngptgp  24664  tngngp  24690  nmoleub  24767  icccmp  24860  reconnlem2  24862  reconn  24863  xmetdcn2  24872  metdseq0  24889  metdscn  24891  elcncf2  24929  cncfmet  24948  cnheibor  25000  nmoleub2lem2  25162  nmoleub3  25165  cvsi  25176  iscfil2  25313  iscfil3  25320  cfilfcls  25321  equivcfil  25346  caubl  25355  bcthlem5  25375  pmltpc  25498  ovollb2  25537  ovoliunnul  25555  ovolicc2lem4  25568  volsup  25604  ioorf  25621  dyadss  25642  dyaddisjlem  25643  mbfposr  25700  cncombf  25706  mbflimsup  25714  i1fmulclem  25751  mbfi1fseqlem4  25767  iblss2  25855  ellimc2  25926  ellimc3  25928  dvnadd  25979  dvmptfsum  26027  dvferm1  26037  dvferm2  26039  fta1g  26223  plyeq0lem  26263  plydivex  26353  fta1  26364  aalioulem2  26389  aalioulem3  26390  ulmuni  26449  ulmbdd  26455  ulmdvlem3  26459  mtest  26461  abelthlem8  26497  efopn  26714  cxpmul2z  26747  cxpcn3lem  26804  jensen  27046  lgambdd  27094  lgamucov  27095  isppw2  27172  mersenne  27285  dchrelbas3  27296  dchrptlem1  27322  dchrpt  27325  lgsval2lem  27365  lgsdchrval  27412  lgsquad3  27445  2sqb  27490  2sqmo  27495  pntrsumbnd2  27625  pntpbnd  27646  pntibnd  27651  nosupno  27762  noinfno  27777  noetasuplem4  27795  noetalem1  27800  madebday  27952  cofcutr  27972  negsprop  28081  mulscom  28179  absmuls  28282  remulscl  28448  tgjustr  28496  tglowdim1i  28523  tgbtwndiff  28528  tgifscgr  28530  iscgrglt  28536  tgcgrxfr  28540  lnext  28589  tgbtwnconn1lem3  28596  tgbtwnconn1  28597  legval  28606  legov  28607  legov2  28608  legtrd  28611  legtri3  28612  legso  28621  hlcgrex  28638  hlcgreu  28640  tglnne  28650  tglndim0  28651  tglineeltr  28653  tglinethru  28658  tglnne0  28662  tglnpt2  28663  colline  28671  tglowdim2l  28672  tglowdim2ln  28673  mirreu3  28676  miriso  28692  midexlem  28714  isperp  28734  perpcom  28735  perpneq  28736  isperp2  28737  footexALT  28740  footex  28743  colperpexlem3  28754  opphllem  28757  midex  28759  oppne3  28765  opptgdim2  28767  opphllem2  28770  opphllem3  28771  opphllem5  28773  opphllem6  28774  opphl  28776  outpasch  28777  lnopp2hpgb  28785  colopp  28791  lmieu  28806  trgcopy  28826  trgcopyeu  28828  iscgra1  28832  cgrane1  28834  cgrane2  28835  cgrane3  28836  cgrahl1  28838  cgrahl2  28839  cgracgr  28840  cgraswap  28842  cgracom  28844  cgratr  28845  flatcgra  28846  cgrabtwn  28848  cgrahl  28849  dfcgra2  28852  sacgr  28853  acopyeu  28856  inaghl  28867  cgrg3col4  28875  f1otrg  28893  f1otrge  28894  axsegcon  28956  axeuclidlem  28991  upgr1eopALT  29148  usgr1eop  29281  pthdepisspth  29767  wpthswwlks2on  29990  clwwlkf1  30077  clwwlknscsh  30090  2pthfrgr  30312  n4cyclfrgr  30319  frgrwopreglem5  30349  frgrwopreglem5ALT  30350  friendshipgt3  30426  smcnlem  30725  0lno  30818  ubthlem1  30898  ubthlem3  30900  chocunii  31329  occl  31332  5oalem1  31682  3oalem2  31691  nmopub2tALT  31937  nmfnleub2  31954  lnconi  32061  kbass5  32148  mdslmd1lem1  32353  mdslmd1lem2  32354  cdj1i  32461  opreu2reuALT  32504  disjabrex  32601  disjabrexf  32602  2ndresdju  32665  acunirnmpt  32675  acunirnmpt2  32676  acunirnmpt2f  32677  aciunf1lem  32678  fnpreimac  32687  fgreu  32688  suppovss  32695  xrge0infss  32770  xrofsup  32777  fsumiunle  32835  s3f1  32915  ccatf1  32917  ccatws1f1o  32920  swrdf1  32925  ressprs  32938  dfmgc2  32970  mgcf1o  32977  chnind  32984  chnso  32987  xrge0addgt0  33004  mndlrinvb  33012  mndlactf1  33013  mndlactfo  33014  mndractf1  33015  mndractfo  33016  mndlactf1o  33017  gsumfs2d  33040  gsumwun  33050  gsumwrd2dccatlem  33051  gsumle  33083  psgnfzto1stlem  33102  fzto1st1  33104  cycpmco2  33135  cycpmrn  33145  cyc3genpm  33154  cycpmconjs  33158  cyc3conja  33159  submarchi  33175  isarchi3  33176  archiabllem1  33182  archiabllem2a  33183  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  erler  33251  rlocaddval  33254  rlocmulval  33255  rloccring  33256  rloc1r  33258  subrdom  33268  isdrng4  33278  fracfld  33289  suborng  33324  isarchiofld  33326  imaslmod  33360  dvdsruasso  33392  unitprodclb  33396  nsgqusf1olem2  33421  lmhmqusker  33424  intlidl  33427  rhmquskerlem  33432  elrspunidl  33435  elrspunsn  33436  rhmimaidl  33439  prmidl2  33448  isprmidlc  33454  rhmpreimaprmidl  33458  qsidomlem2  33460  ssdifidllem  33463  ssdifidlprm  33465  mxidlprm  33477  ssmxidl  33481  opprqusplusg  33496  opprqusmulr  33498  qsdrngilem  33501  qsdrngi  33502  rsprprmprmidl  33529  rsprprmprmidlb  33530  rprmirred  33538  rprmirredb  33539  rprmdvdspow  33540  rprmdvdsprod  33541  1arithidom  33544  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  dfufd2lem  33556  dfufd2  33557  zringfrac  33561  ply1dg3rt0irred  33586  r1plmhm  33609  r1pquslmic  33610  lindsunlem  33651  lindsun  33652  dimkerim  33654  fedgmullem1  33656  fedgmul  33658  dimlssid  33659  evls1fldgencl  33694  minplyirred  33718  fldext2chn  33733  constrmon  33748  constrconj  33749  constrfin  33750  constrelextdg2  33751  mdetpmtr1  33783  txomap  33794  qtophaus  33796  cmpcref  33810  zarclsun  33830  zarclssn  33833  zarcmplem  33841  pstmxmet  33857  sqsscirc1  33868  ordtrest2NEWlem  33882  ordtconnlem1  33884  pnfneige0  33911  lmxrge0  33912  lmdvg  33913  qqhval2  33944  esumcst  34043  esumrnmpt2  34048  esumfsup  34050  esumcvg  34066  esum2d  34073  esumiun  34074  sigaclfu2  34101  insiga  34117  ldsysgenld  34140  ldgenpisyslem1  34143  fiunelros  34154  measinb  34201  imambfm  34243  oms0  34278  omssubadd  34281  carsgclctunlem3  34301  eulerpartlemgvv  34357  dstrvprob  34452  sgnsub  34525  signstfvneq0  34565  actfunsnrndisj  34598  reprinfz1  34615  breprexp  34626  afsval  34664  derangenlem  35155  sconnpi1  35223  cvmsss2  35258  cvmopnlem  35262  cvmlift3lem7  35309  msrval  35522  ifscgr  36025  cgrxfr  36036  btwnconn1lem13  36080  outsideofeu  36112  neibastop2lem  36342  weiunso  36448  irrdifflemf  37307  irrdiff  37308  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem14  37620  poimirlem22  37628  poimirlem29  37635  broucube  37640  heicant  37641  mblfinlem1  37643  itg2addnclem  37657  ftc1cnnc  37678  ftc1anclem7  37685  sstotbnd2  37760  equivtotbnd  37764  isbnd3  37770  ssbnd  37774  totbndbnd  37775  cntotbnd  37782  heibor1lem  37795  rrncmslem  37818  lssats  38993  lsat0cv  39014  lkrlss  39076  lfl1dim  39102  lfl1dim2N  39103  lkrpssN  39144  hlhgt2  39371  3dim2  39450  2dim  39452  lplncvrlvol  39598  paddasslem11  39812  pmapjat1  39835  2polssN  39897  pclfinclN  39932  pexmidlem8N  39959  lhpexle1lem  39989  4atex  40058  ltrnid  40117  trlator0  40153  cdlemg2cex  40573  tendodi1  40766  tendodi2  40767  diblss  41152  dihopelvalcpre  41230  dihatexv  41320  mapdval4N  41614  fldhmf1  42071  mndmolinv  42076  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij2  42084  primrootspoweq0  42087  aks6d1c2p2  42100  hashscontpow  42103  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5  42120  sticksstones8  42134  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem3  42153  aks6d1c6isolem1  42155  unitscyglem3  42178  aks5  42185  metakunt1  42186  metakunt2  42187  sn-subeu  42432  sn-0tie0  42445  fiabv  42522  frlmsnic  42526  fsuppind  42576  prjspersym  42593  dffltz  42620  nna4b4nsq  42646  mzpindd  42733  mzpsubst  42735  mzpcompact2lem  42738  eldioph2b  42750  irrapxlem3  42811  irrapxlem5  42813  pellex  42822  pell1234qrdich  42848  pell14qrexpcl  42854  congabseq  42962  jm2.26a  42988  jm2.26lem3  42989  rmydioph  43002  lnrfg  43107  hbt  43118  cantnftermord  43309  cantnfresb  43313  cantnf2  43314  oawordex2  43315  omabs2  43321  tfsconcatfv  43330  tfsconcatrev  43337  ofoaass  43349  nadd2rabtr  43373  nadd1suc  43381  naddgeoa  43383  rfovcnvf1od  43993  clsk3nimkb  44029  ntrneiiso  44080  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  4an4132  44496  iunconnlem2  44932  modelaxrep  44945  fnchoice  44966  cncmpmax  44969  ssinc  45026  ssdec  45027  disjf1  45125  supxrge  45287  suplesup  45288  infxr  45316  infleinf  45321  unb2ltle  45364  rexabslelem  45367  uzub  45380  supminfxr  45413  climrec  45558  climsuse  45563  islptre  45574  addlimc  45603  0ellimcdiv  45604  limsuppnfdlem  45656  limsupub  45659  limsuppnflem  45665  limsupubuz  45668  climinf3  45671  limsupmnflem  45675  climxrre  45705  liminfreuzlem  45757  liminflimsupclim  45762  xlimliminflimsup  45817  icccncfext  45842  cncfiooicclem1  45848  fperdvper  45874  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvmptfprodlem  45899  dvmptfprod  45900  dvnprodlem2  45902  stoweidlem7  45962  stoweidlem34  45989  stoweidlem52  46007  stoweidlem60  46015  wallispilem3  46022  fourierdlem34  46096  fourierdlem38  46100  fourierdlem39  46101  fourierdlem48  46109  fourierdlem50  46111  fourierdlem51  46112  fourierdlem73  46134  fourierdlem76  46137  fourierdlem77  46138  fourierdlem80  46141  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  etransclem32  46221  etransclem33  46222  sge0f1o  46337  sge0pr  46349  sge0isum  46382  iundjiun  46415  meaiininclem  46441  pimdecfgtioo  46672  pimincfltioo  46673  preimageiingt  46675  preimaleiinlt  46676  smflimlem2  46727  smflimlem4  46729  smfmullem3  46748  smflimmpt  46765  smfinflem  46772  smfpimne2  46795  fsupdm  46797  finfdm  46801  cfsetsnfsetfo  47009  funressnbrafv2  47193  imasetpreimafvbijlemf1  47328  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbnd  47733  isuspgrim  47812  stgrusgra  47861  isubgr3stgrlem6  47873  2zlidl  48083  lindslinindsimp2  48308  snlindsntor  48316  lincresunit2  48323  islindeps2  48328