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  6361  fsnex  7303  soisoi  7348  f1o2ndf1  8147  fimaproj  8160  fprlem2  8326  tz7.49  8485  omabs  8689  cofon1  8710  naddssim  8723  omxpenlem  9113  fopwdom  9120  findcard3  9318  findcard3OLD  9319  frfi  9321  finsschain  9399  marypha1lem  9473  wemappo  9589  wdomtr  9615  cantnfp1  9721  ttrcltr  9756  harcard  10018  numacn  10089  infunsdom1  10252  sornom  10317  ssfin4  10350  fin1a2lem11  10450  fin1a2lem13  10452  fpwwe2lem12  10682  pwfseq  10704  mulcmpblnr  11111  00id  11436  addrid  11441  cnegex  11442  negeu  11498  add20  11775  ltmul12a  12123  lediv12a  12161  cru  12258  qextltlem  13244  xleadd1a  13295  xmullem  13306  xlemul1a  13330  ixxss12  13407  ioodisj  13522  fvf1tp  13829  fsuppmapnn0fz  14037  seqf1o  14084  mulexpz  14143  leexp1a  14215  faclbnd  14329  swrdswrdlem  14742  abs3lem  15377  rexico  15392  cau3lem  15393  rlim3  15534  ello12  15552  lo1bdd2  15560  elo12  15563  rlimconst  15580  isercoll  15704  climcau  15707  climbdd  15708  summolem2  15752  fsumconst  15826  o1fsum  15849  incexclem  15872  fprodconst  16014  bitsfzo  16472  dvdsmulgcd  16593  pc2dvds  16917  pcz  16919  pcadd  16927  pcfac  16937  vdwmc2  17017  vdwlem2  17020  vdwlem10  17028  vdw  17032  ramcl  17067  sbcie3s  17199  firest  17477  prdsval  17500  mreexd  17685  mreexexlemd  17687  iscat  17715  cidfval  17719  iscatd2  17724  catcocl  17728  catass  17729  catpropd  17752  cidpropd  17753  moni  17780  monpropd  17781  issubc  17880  subccocl  17890  funcco  17916  funcpropd  17947  fullpropd  17967  nati  18003  natpropd  18024  fucpropd  18025  xpcpropd  18253  curfuncf  18283  curf2ndf  18292  yonffthlem  18327  acsfiindd  18598  mgmhmeql  18729  sgrppropd  18744  mndpropd  18772  mhmeql  18839  smndex1mgm  18920  isgrpinv  19011  dfgrp3lem  19056  mhmmnd  19082  cycsubm  19220  cycsubmcom  19222  conjnmzb  19271  ghmqusnsg  19300  ghmquskerlem3  19304  ghmqusker  19305  gass  19319  symgextf  19435  dfod2  19582  gexdvds  19602  sylow3lem2  19646  efgredlem  19765  efgredeu  19770  ghmcmn  19849  oddvdssubg  19873  dprdfcntz  20035  pgpfaclem3  20103  isrng  20151  issrg  20185  isring  20234  dvdsrmul1  20369  issubdrg  20781  islmhm2  21037  lmhmeql  21054  lssacsex  21146  rhmpreimaidl  21287  rhmqusnsg  21295  isphl  21646  uvcf1  21812  lindfmm  21847  sraassab  21888  issubassa2  21912  opsrval  22064  psdmul  22170  scmatmats  22517  smatvscl  22530  mdetunilem7  22624  gsummatr01lem4  22664  m2cpmfo  22762  pmatcollpw3fi1lem1  22792  pm2mpf1lem  22800  pm2mpf1  22805  mp2pm2mplem4  22815  pm2mpghm  22822  chfacfscmulfsupp  22865  chfacfpmmulfsupp  22869  cctop  23013  neiptoptop  23139  neiptopreu  23141  tgrest  23167  ordtrest2lem  23211  cnss1  23284  cncnp  23288  isnrm3  23367  uncmp  23411  cmpfi  23416  iunconn  23436  1stcrest  23461  subislly  23489  islly2  23492  cldllycmp  23503  lly1stc  23504  llycmpkgen2  23558  kgencn  23564  xkoccn  23627  ptcnplem  23629  pthaus  23646  txhaus  23655  txkgen  23660  xkohaus  23661  xkococnlem  23667  txconn  23697  regr1lem2  23748  kqreglem1  23749  reghmph  23801  nrmhmph  23802  trfil2  23895  ufileu  23927  flimopn  23983  flimcf  23990  fclscf  24033  ufilcmp  24040  cnpfcf  24049  cnextfun  24072  tgpmulg  24101  symgtgp  24114  tgpt0  24127  qustgplem  24129  ustex2sym  24225  ustex3sym  24226  trust  24238  restutop  24246  restutopopn  24247  ustuqtop4  24253  utop3cls  24260  utopreg  24261  cstucnd  24293  ucncn  24294  trcfilu  24303  neipcfilu  24305  ismet2  24343  metequiv2  24523  metcnp  24554  metcnp2  24555  metcnpi3  24559  txmetcnp  24560  metustto  24566  metustsym  24568  metust  24571  cfilucfil  24572  metuel2  24578  psmetutop  24580  restmetu  24583  metucn  24584  ngptgp  24649  tngngp  24675  nmoleub  24752  icccmp  24847  reconnlem2  24849  reconn  24850  xmetdcn2  24859  metdseq0  24876  metdscn  24878  elcncf2  24916  cncfmet  24935  cnheibor  24987  nmoleub2lem2  25149  nmoleub3  25152  cvsi  25163  iscfil2  25300  iscfil3  25307  cfilfcls  25308  equivcfil  25333  caubl  25342  bcthlem5  25362  pmltpc  25485  ovollb2  25524  ovoliunnul  25542  ovolicc2lem4  25555  volsup  25591  ioorf  25608  dyadss  25629  dyaddisjlem  25630  mbfposr  25687  cncombf  25693  mbflimsup  25701  i1fmulclem  25737  mbfi1fseqlem4  25753  iblss2  25841  ellimc2  25912  ellimc3  25914  dvnadd  25965  dvmptfsum  26013  dvferm1  26023  dvferm2  26025  fta1g  26209  plyeq0lem  26249  plydivex  26339  fta1  26350  aalioulem2  26375  aalioulem3  26376  ulmuni  26435  ulmbdd  26441  ulmdvlem3  26445  mtest  26447  abelthlem8  26483  efopn  26700  cxpmul2z  26733  cxpcn3lem  26790  jensen  27032  lgambdd  27080  lgamucov  27081  isppw2  27158  mersenne  27271  dchrelbas3  27282  dchrptlem1  27308  dchrpt  27311  lgsval2lem  27351  lgsdchrval  27398  lgsquad3  27431  2sqb  27476  2sqmo  27481  pntrsumbnd2  27611  pntpbnd  27632  pntibnd  27637  nosupno  27748  noinfno  27763  noetasuplem4  27781  noetalem1  27786  madebday  27938  cofcutr  27958  negsprop  28067  mulscom  28165  absmuls  28268  remulscl  28434  tgjustr  28482  tglowdim1i  28509  tgbtwndiff  28514  tgifscgr  28516  iscgrglt  28522  tgcgrxfr  28526  lnext  28575  tgbtwnconn1lem3  28582  tgbtwnconn1  28583  legval  28592  legov  28593  legov2  28594  legtrd  28597  legtri3  28598  legso  28607  hlcgrex  28624  hlcgreu  28626  tglnne  28636  tglndim0  28637  tglineeltr  28639  tglinethru  28644  tglnne0  28648  tglnpt2  28649  colline  28657  tglowdim2l  28658  tglowdim2ln  28659  mirreu3  28662  miriso  28678  midexlem  28700  isperp  28720  perpcom  28721  perpneq  28722  isperp2  28723  footexALT  28726  footex  28729  colperpexlem3  28740  opphllem  28743  midex  28745  oppne3  28751  opptgdim2  28753  opphllem2  28756  opphllem3  28757  opphllem5  28759  opphllem6  28760  opphl  28762  outpasch  28763  lnopp2hpgb  28771  colopp  28777  lmieu  28792  trgcopy  28812  trgcopyeu  28814  iscgra1  28818  cgrane1  28820  cgrane2  28821  cgrane3  28822  cgrahl1  28824  cgrahl2  28825  cgracgr  28826  cgraswap  28828  cgracom  28830  cgratr  28831  flatcgra  28832  cgrabtwn  28834  cgrahl  28835  dfcgra2  28838  sacgr  28839  acopyeu  28842  inaghl  28853  cgrg3col4  28861  f1otrg  28879  f1otrge  28880  axsegcon  28942  axeuclidlem  28977  upgr1eopALT  29134  usgr1eop  29267  pthdepisspth  29755  wpthswwlks2on  29981  clwwlkf1  30068  clwwlknscsh  30081  2pthfrgr  30303  n4cyclfrgr  30310  frgrwopreglem5  30340  frgrwopreglem5ALT  30341  friendshipgt3  30417  smcnlem  30716  0lno  30809  ubthlem1  30889  ubthlem3  30891  chocunii  31320  occl  31323  5oalem1  31673  3oalem2  31682  nmopub2tALT  31928  nmfnleub2  31945  lnconi  32052  kbass5  32139  mdslmd1lem1  32344  mdslmd1lem2  32345  cdj1i  32452  opreu2reuALT  32496  disjabrex  32595  disjabrexf  32596  2ndresdju  32659  acunirnmpt  32669  acunirnmpt2  32670  acunirnmpt2f  32671  aciunf1lem  32672  fnpreimac  32681  fgreu  32682  suppovss  32690  xrge0infss  32764  xrofsup  32771  fsumiunle  32831  2exple2exp  32834  s3f1  32931  ccatf1  32933  ccatws1f1o  32936  swrdf1  32941  ressprs  32954  dfmgc2  32986  mgcf1o  32993  chnind  33001  chnso  33004  xrge0addgt0  33022  mndlrinvb  33030  mndlactf1  33031  mndlactfo  33032  mndractf1  33033  mndractfo  33034  mndlactf1o  33035  gsumfs2d  33058  gsumwun  33068  gsumwrd2dccatlem  33069  gsumle  33101  psgnfzto1stlem  33120  fzto1st1  33122  cycpmco2  33153  cycpmrn  33163  cyc3genpm  33172  cycpmconjs  33176  cyc3conja  33177  submarchi  33193  isarchi3  33194  archiabllem1  33200  archiabllem2a  33201  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem2  33252  erler  33269  rlocaddval  33272  rlocmulval  33273  rloccring  33274  rloc1r  33276  subrdom  33288  isdrng4  33298  fracfld  33310  suborng  33345  isarchiofld  33347  imaslmod  33381  dvdsruasso  33413  unitprodclb  33417  nsgqusf1olem2  33442  lmhmqusker  33445  intlidl  33448  rhmquskerlem  33453  elrspunidl  33456  elrspunsn  33457  rhmimaidl  33460  prmidl2  33469  isprmidlc  33475  rhmpreimaprmidl  33479  qsidomlem2  33481  ssdifidllem  33484  ssdifidlprm  33486  mxidlprm  33498  ssmxidl  33502  opprqusplusg  33517  opprqusmulr  33519  qsdrngilem  33522  qsdrngi  33523  rsprprmprmidl  33550  rsprprmprmidlb  33551  rprmirred  33559  rprmirredb  33560  rprmdvdspow  33561  rprmdvdsprod  33562  1arithidom  33565  1arithufdlem2  33573  1arithufdlem3  33574  1arithufdlem4  33575  dfufd2lem  33577  dfufd2  33578  zringfrac  33582  ply1dg3rt0irred  33607  r1plmhm  33630  r1pquslmic  33631  exsslsb  33647  lindsunlem  33675  lindsun  33676  dimkerim  33678  fedgmullem1  33680  fedgmul  33682  dimlssid  33683  evls1fldgencl  33720  fldextrspunlsplem  33723  minplyirred  33754  fldext2chn  33769  constrmon  33785  constrconj  33786  constrfin  33787  constrelextdg2  33788  constrextdg2lem  33789  constrextdg2  33790  mdetpmtr1  33822  txomap  33833  qtophaus  33835  cmpcref  33849  zarclsun  33869  zarclssn  33872  zarcmplem  33880  pstmxmet  33896  sqsscirc1  33907  ordtrest2NEWlem  33921  ordtconnlem1  33923  pnfneige0  33950  lmxrge0  33951  lmdvg  33952  qqhval2  33983  esumcst  34064  esumrnmpt2  34069  esumfsup  34071  esumcvg  34087  esum2d  34094  esumiun  34095  sigaclfu2  34122  insiga  34138  ldsysgenld  34161  ldgenpisyslem1  34164  fiunelros  34175  measinb  34222  imambfm  34264  oms0  34299  omssubadd  34302  carsgclctunlem3  34322  eulerpartlemgvv  34378  dstrvprob  34474  sgnsub  34547  signstfvneq0  34587  actfunsnrndisj  34620  reprinfz1  34637  breprexp  34648  afsval  34686  derangenlem  35176  sconnpi1  35244  cvmsss2  35279  cvmopnlem  35283  cvmlift3lem7  35330  msrval  35543  ifscgr  36045  cgrxfr  36056  btwnconn1lem13  36100  outsideofeu  36132  neibastop2lem  36361  weiunso  36467  irrdifflemf  37326  irrdiff  37327  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem14  37641  poimirlem22  37649  poimirlem29  37656  broucube  37661  heicant  37662  mblfinlem1  37664  itg2addnclem  37678  ftc1cnnc  37699  ftc1anclem7  37706  sstotbnd2  37781  equivtotbnd  37785  isbnd3  37791  ssbnd  37795  totbndbnd  37796  cntotbnd  37803  heibor1lem  37816  rrncmslem  37839  lssats  39013  lsat0cv  39034  lkrlss  39096  lfl1dim  39122  lfl1dim2N  39123  lkrpssN  39164  hlhgt2  39391  3dim2  39470  2dim  39472  lplncvrlvol  39618  paddasslem11  39832  pmapjat1  39855  2polssN  39917  pclfinclN  39952  pexmidlem8N  39979  lhpexle1lem  40009  4atex  40078  ltrnid  40137  trlator0  40173  cdlemg2cex  40593  tendodi1  40786  tendodi2  40787  diblss  41172  dihopelvalcpre  41250  dihatexv  41340  mapdval4N  41634  fldhmf1  42091  mndmolinv  42096  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij2  42104  primrootspoweq0  42107  aks6d1c2p2  42120  hashscontpow  42123  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5  42140  sticksstones8  42154  sticksstones12  42159  sticksstones22  42169  aks6d1c6lem3  42173  aks6d1c6isolem1  42175  unitscyglem3  42198  aks5  42205  metakunt1  42206  metakunt2  42207  sn-subeu  42456  sn-0tie0  42469  fiabv  42546  frlmsnic  42550  fsuppind  42600  prjspersym  42617  dffltz  42644  nna4b4nsq  42670  mzpindd  42757  mzpsubst  42759  mzpcompact2lem  42762  eldioph2b  42774  irrapxlem3  42835  irrapxlem5  42837  pellex  42846  pell1234qrdich  42872  pell14qrexpcl  42878  congabseq  42986  jm2.26a  43012  jm2.26lem3  43013  rmydioph  43026  lnrfg  43131  hbt  43142  cantnftermord  43333  cantnfresb  43337  cantnf2  43338  oawordex2  43339  omabs2  43345  tfsconcatfv  43354  tfsconcatrev  43361  ofoaass  43373  nadd2rabtr  43397  nadd1suc  43405  naddgeoa  43407  rfovcnvf1od  44017  clsk3nimkb  44053  ntrneiiso  44104  ntrneikb  44107  ntrneixb  44108  ntrneik3  44109  ntrneix3  44110  ntrneik13  44111  ntrneix13  44112  4an4132  44519  iunconnlem2  44955  modelaxrep  44998  fnchoice  45034  cncmpmax  45037  ssinc  45092  ssdec  45093  disjf1  45188  supxrge  45349  suplesup  45350  infxr  45378  infleinf  45383  unb2ltle  45426  rexabslelem  45429  uzub  45442  supminfxr  45475  climrec  45618  climsuse  45623  islptre  45634  addlimc  45663  0ellimcdiv  45664  limsuppnfdlem  45716  limsupub  45719  limsuppnflem  45725  limsupubuz  45728  climinf3  45731  limsupmnflem  45735  climxrre  45765  liminfreuzlem  45817  liminflimsupclim  45822  xlimliminflimsup  45877  icccncfext  45902  cncfiooicclem1  45908  fperdvper  45934  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvmptfprodlem  45959  dvmptfprod  45960  dvnprodlem2  45962  stoweidlem7  46022  stoweidlem34  46049  stoweidlem52  46067  stoweidlem60  46075  wallispilem3  46082  fourierdlem34  46156  fourierdlem38  46160  fourierdlem39  46161  fourierdlem48  46169  fourierdlem50  46171  fourierdlem51  46172  fourierdlem73  46194  fourierdlem76  46197  fourierdlem77  46198  fourierdlem80  46201  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  etransclem32  46281  etransclem33  46282  sge0f1o  46397  sge0pr  46409  sge0isum  46442  iundjiun  46475  meaiininclem  46501  pimdecfgtioo  46732  pimincfltioo  46733  preimageiingt  46735  preimaleiinlt  46736  smflimlem2  46787  smflimlem4  46789  smfmullem3  46808  smflimmpt  46825  smfinflem  46832  smfpimne2  46855  fsupdm  46857  finfdm  46861  cfsetsnfsetfo  47072  funressnbrafv2  47256  imasetpreimafvbijlemf1  47391  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbnd  47796  isuspgrim  47875  stgrusgra  47926  isubgr3stgrlem6  47938  2zlidl  48156  lindslinindsimp2  48380  snlindsntor  48388  lincresunit2  48395  islindeps2  48400  fucofvalg  49013  fuco21  49031  precofvalALT  49063