Theorem simpllr 775

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  6292  fsnex  7224  soisoi  7269  f1o2ndf1  8062  fimaproj  8075  fprlem2  8241  tz7.49  8374  omabs  8576  cofon1  8597  naddssim  8610  omxpenlem  9002  fopwdom  9009  findcard3  9187  findcard3OLD  9188  frfi  9190  finsschain  9268  marypha1lem  9342  wemappo  9460  wdomtr  9486  cantnfp1  9596  ttrcltr  9631  harcard  9893  numacn  9962  infunsdom1  10125  sornom  10190  ssfin4  10223  fin1a2lem11  10323  fin1a2lem13  10325  fpwwe2lem12  10555  pwfseq  10577  mulcmpblnr  10984  00id  11309  addrid  11314  cnegex  11315  negeu  11371  add20  11650  ltmul12a  11998  lediv12a  12036  cru  12138  qextltlem  13122  xleadd1a  13173  xmullem  13184  xlemul1a  13208  ixxss12  13286  ioodisj  13403  fvf1tp  13711  fsuppmapnn0fz  13921  seqf1o  13968  mulexpz  14027  leexp1a  14100  faclbnd  14215  swrdswrdlem  14628  abs3lem  15264  rexico  15279  cau3lem  15280  rlim3  15423  ello12  15441  lo1bdd2  15449  elo12  15452  rlimconst  15469  isercoll  15593  climcau  15596  climbdd  15597  summolem2  15641  fsumconst  15715  o1fsum  15738  incexclem  15761  fprodconst  15903  bitsfzo  16364  dvdsmulgcd  16485  pc2dvds  16809  pcz  16811  pcadd  16819  pcfac  16829  vdwmc2  16909  vdwlem2  16912  vdwlem10  16920  vdw  16924  ramcl  16959  sbcie3s  17091  firest  17354  prdsval  17377  mreexd  17566  mreexexlemd  17568  iscat  17596  cidfval  17600  iscatd2  17605  catcocl  17609  catass  17610  catpropd  17633  cidpropd  17634  moni  17661  monpropd  17662  issubc  17760  subccocl  17770  funcco  17796  funcpropd  17827  fullpropd  17847  nati  17883  natpropd  17904  fucpropd  17905  xpcpropd  18132  curfuncf  18162  curf2ndf  18171  yonffthlem  18206  acsfiindd  18477  mgmhmeql  18608  sgrppropd  18623  mndpropd  18651  mhmeql  18718  smndex1mgm  18799  isgrpinv  18890  dfgrp3lem  18935  mhmmnd  18961  cycsubm  19099  cycsubmcom  19101  conjnmzb  19150  ghmqusnsg  19179  ghmquskerlem3  19183  ghmqusker  19184  gass  19198  symgextf  19314  dfod2  19461  gexdvds  19481  sylow3lem2  19525  efgredlem  19644  efgredeu  19649  ghmcmn  19728  oddvdssubg  19752  dprdfcntz  19914  pgpfaclem3  19982  gsumle  20042  isrng  20057  issrg  20091  isring  20140  dvdsrmul1  20272  issubdrg  20683  suborng  20779  islmhm2  20960  lmhmeql  20977  lssacsex  21069  rhmpreimaidl  21202  rhmqusnsg  21210  isphl  21553  uvcf1  21717  lindfmm  21752  sraassab  21793  issubassa2  21817  opsrval  21969  psdmul  22069  scmatmats  22414  smatvscl  22427  mdetunilem7  22521  gsummatr01lem4  22561  m2cpmfo  22659  pmatcollpw3fi1lem1  22689  pm2mpf1lem  22697  pm2mpf1  22702  mp2pm2mplem4  22712  pm2mpghm  22719  chfacfscmulfsupp  22762  chfacfpmmulfsupp  22766  cctop  22909  neiptoptop  23034  neiptopreu  23036  tgrest  23062  ordtrest2lem  23106  cnss1  23179  cncnp  23183  isnrm3  23262  uncmp  23306  cmpfi  23311  iunconn  23331  1stcrest  23356  subislly  23384  islly2  23387  cldllycmp  23398  lly1stc  23399  llycmpkgen2  23453  kgencn  23459  xkoccn  23522  ptcnplem  23524  pthaus  23541  txhaus  23550  txkgen  23555  xkohaus  23556  xkococnlem  23562  txconn  23592  regr1lem2  23643  kqreglem1  23644  reghmph  23696  nrmhmph  23697  trfil2  23790  ufileu  23822  flimopn  23878  flimcf  23885  fclscf  23928  ufilcmp  23935  cnpfcf  23944  cnextfun  23967  tgpmulg  23996  symgtgp  24009  tgpt0  24022  qustgplem  24024  ustex2sym  24120  ustex3sym  24121  trust  24133  restutop  24141  restutopopn  24142  ustuqtop4  24148  utop3cls  24155  utopreg  24156  cstucnd  24187  ucncn  24188  trcfilu  24197  neipcfilu  24199  ismet2  24237  metequiv2  24414  metcnp  24445  metcnp2  24446  metcnpi3  24450  txmetcnp  24451  metustto  24457  metustsym  24459  metust  24462  cfilucfil  24463  metuel2  24469  psmetutop  24471  restmetu  24474  metucn  24475  ngptgp  24540  tngngp  24558  nmoleub  24635  icccmp  24730  reconnlem2  24732  reconn  24733  xmetdcn2  24742  metdseq0  24759  metdscn  24761  elcncf2  24799  cncfmet  24818  cnheibor  24870  nmoleub2lem2  25032  nmoleub3  25035  cvsi  25046  iscfil2  25182  iscfil3  25189  cfilfcls  25190  equivcfil  25215  caubl  25224  bcthlem5  25244  pmltpc  25367  ovollb2  25406  ovoliunnul  25424  ovolicc2lem4  25437  volsup  25473  ioorf  25490  dyadss  25511  dyaddisjlem  25512  mbfposr  25569  cncombf  25575  mbflimsup  25583  i1fmulclem  25619  mbfi1fseqlem4  25635  iblss2  25723  ellimc2  25794  ellimc3  25796  dvnadd  25847  dvmptfsum  25895  dvferm1  25905  dvferm2  25907  fta1g  26091  plyeq0lem  26131  plydivex  26221  fta1  26232  aalioulem2  26257  aalioulem3  26258  ulmuni  26317  ulmbdd  26323  ulmdvlem3  26327  mtest  26329  abelthlem8  26365  efopn  26583  cxpmul2z  26616  cxpcn3lem  26673  jensen  26915  lgambdd  26963  lgamucov  26964  isppw2  27041  mersenne  27154  dchrelbas3  27165  dchrptlem1  27191  dchrpt  27194  lgsval2lem  27234  lgsdchrval  27281  lgsquad3  27314  2sqb  27359  2sqmo  27364  pntrsumbnd2  27494  pntpbnd  27515  pntibnd  27520  nosupno  27631  noinfno  27646  noetasuplem4  27664  noetalem1  27669  madebday  27832  cofcutr  27855  negsprop  27964  mulscom  28065  absmuls  28169  zs12ge0  28378  remulscl  28389  tgjustr  28437  tglowdim1i  28464  tgbtwndiff  28469  tgifscgr  28471  iscgrglt  28477  tgcgrxfr  28481  lnext  28530  tgbtwnconn1lem3  28537  tgbtwnconn1  28538  legval  28547  legov  28548  legov2  28549  legtrd  28552  legtri3  28553  legso  28562  hlcgrex  28579  hlcgreu  28581  tglnne  28591  tglndim0  28592  tglineeltr  28594  tglinethru  28599  tglnne0  28603  tglnpt2  28604  colline  28612  tglowdim2l  28613  tglowdim2ln  28614  mirreu3  28617  miriso  28633  midexlem  28655  isperp  28675  perpcom  28676  perpneq  28677  isperp2  28678  footexALT  28681  footex  28684  colperpexlem3  28695  opphllem  28698  midex  28700  oppne3  28706  opptgdim2  28708  opphllem2  28711  opphllem3  28712  opphllem5  28714  opphllem6  28715  opphl  28717  outpasch  28718  lnopp2hpgb  28726  colopp  28732  lmieu  28747  trgcopy  28767  trgcopyeu  28769  iscgra1  28773  cgrane1  28775  cgrane2  28776  cgrane3  28777  cgrahl1  28779  cgrahl2  28780  cgracgr  28781  cgraswap  28783  cgracom  28785  cgratr  28786  flatcgra  28787  cgrabtwn  28789  cgrahl  28790  dfcgra2  28793  sacgr  28794  acopyeu  28797  inaghl  28808  cgrg3col4  28816  f1otrg  28834  f1otrge  28835  axsegcon  28890  axeuclidlem  28925  upgr1eopALT  29080  usgr1eop  29213  pthdepisspth  29698  wpthswwlks2on  29924  clwwlkf1  30011  clwwlknscsh  30024  2pthfrgr  30246  n4cyclfrgr  30253  frgrwopreglem5  30283  frgrwopreglem5ALT  30284  friendshipgt3  30360  smcnlem  30659  0lno  30752  ubthlem1  30832  ubthlem3  30834  chocunii  31263  occl  31266  5oalem1  31616  3oalem2  31625  nmopub2tALT  31871  nmfnleub2  31888  lnconi  31995  kbass5  32082  mdslmd1lem1  32287  mdslmd1lem2  32288  cdj1i  32395  opreu2reuALT  32439  disjabrex  32544  disjabrexf  32545  2ndresdju  32606  acunirnmpt  32616  acunirnmpt2  32617  acunirnmpt2f  32618  aciunf1lem  32619  fnpreimac  32628  fgreu  32629  suppovss  32637  xrge0infss  32716  xrofsup  32723  elq2  32769  fsumiunle  32787  sgnsub  32795  2exple2exp  32803  s3f1  32901  ccatf1  32903  ccatws1f1o  32906  swrdf1  32911  ressprs  32921  dfmgc2  32951  mgcf1o  32958  chnind  32966  chnso  32969  xrge0addgt0  32984  mndlrinvb  32992  mndlactf1  32993  mndlactfo  32994  mndractf1  32995  mndractfo  32996  mndlactf1o  32997  gsumfs2d  33021  gsumwun  33031  gsumwrd2dccatlem  33032  psgnfzto1stlem  33055  fzto1st1  33057  cycpmco2  33088  cycpmrn  33098  cyc3genpm  33107  cycpmconjs  33111  cyc3conja  33112  conjga  33125  submarchi  33138  isarchi3  33139  archiabllem1  33145  archiabllem2a  33146  isarchiofld  33151  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnlem4  33195  elrgspnsubrunlem2  33198  erler  33215  rlocaddval  33218  rlocmulval  33219  rloccring  33220  rloc1r  33222  subrdom  33234  isdrng4  33244  fracfld  33257  imaslmod  33300  dvdsruasso  33332  unitprodclb  33336  nsgqusf1olem2  33361  lmhmqusker  33364  intlidl  33367  rhmquskerlem  33372  elrspunidl  33375  elrspunsn  33376  rhmimaidl  33379  prmidl2  33388  isprmidlc  33394  rhmpreimaprmidl  33398  qsidomlem2  33400  ssdifidllem  33403  ssdifidlprm  33405  mxidlprm  33417  ssmxidl  33421  opprqusplusg  33436  opprqusmulr  33438  qsdrngilem  33441  qsdrngi  33442  rsprprmprmidl  33469  rsprprmprmidlb  33470  rprmirred  33478  rprmirredb  33479  rprmdvdspow  33480  rprmdvdsprod  33481  1arithidom  33484  1arithufdlem2  33492  1arithufdlem3  33493  1arithufdlem4  33494  dfufd2lem  33496  dfufd2  33497  zringfrac  33501  ply1dg3rt0irred  33527  r1plmhm  33551  r1pquslmic  33552  exsslsb  33568  lindsunlem  33596  lindsun  33597  dimkerim  33599  fedgmullem1  33601  fedgmul  33603  dimlssid  33604  evls1fldgencl  33641  fldextrspunlsplem  33644  minplyirred  33677  fldext2chn  33694  constrmon  33710  constrconj  33711  constrfin  33712  constrelextdg2  33713  constrextdg2lem  33714  constrextdg2  33715  constrext2chnlem  33716  constrfiss  33717  cos9thpiminplylem2  33749  mdetpmtr1  33789  txomap  33800  qtophaus  33802  cmpcref  33816  zarclsun  33836  zarclssn  33839  zarcmplem  33847  pstmxmet  33863  sqsscirc1  33874  ordtrest2NEWlem  33888  ordtconnlem1  33890  pnfneige0  33917  lmxrge0  33918  lmdvg  33919  qqhval2  33948  esumcst  34029  esumrnmpt2  34034  esumfsup  34036  esumcvg  34052  esum2d  34059  esumiun  34060  sigaclfu2  34087  insiga  34103  ldsysgenld  34126  ldgenpisyslem1  34129  fiunelros  34140  measinb  34187  imambfm  34229  oms0  34264  omssubadd  34267  carsgclctunlem3  34287  eulerpartlemgvv  34343  dstrvprob  34439  signstfvneq0  34539  actfunsnrndisj  34572  reprinfz1  34589  breprexp  34600  afsval  34638  derangenlem  35143  sconnpi1  35211  cvmsss2  35246  cvmopnlem  35250  cvmlift3lem7  35297  msrval  35510  ifscgr  36017  cgrxfr  36028  btwnconn1lem13  36072  outsideofeu  36104  neibastop2lem  36333  weiunso  36439  irrdifflemf  37298  irrdiff  37299  matunitlindflem1  37595  matunitlindflem2  37596  poimirlem14  37613  poimirlem22  37621  poimirlem29  37628  broucube  37633  heicant  37634  mblfinlem1  37636  itg2addnclem  37650  ftc1cnnc  37671  ftc1anclem7  37678  sstotbnd2  37753  equivtotbnd  37757  isbnd3  37763  ssbnd  37767  totbndbnd  37768  cntotbnd  37775  heibor1lem  37788  rrncmslem  37811  lssats  38990  lsat0cv  39011  lkrlss  39073  lfl1dim  39099  lfl1dim2N  39100  lkrpssN  39141  hlhgt2  39368  3dim2  39447  2dim  39449  lplncvrlvol  39595  paddasslem11  39809  pmapjat1  39832  2polssN  39894  pclfinclN  39929  pexmidlem8N  39956  lhpexle1lem  39986  4atex  40055  ltrnid  40114  trlator0  40150  cdlemg2cex  40570  tendodi1  40763  tendodi2  40764  diblss  41149  dihopelvalcpre  41227  dihatexv  41317  mapdval4N  41611  fldhmf1  42063  mndmolinv  42068  primrootscoprmpow  42072  posbezout  42073  primrootscoprbij2  42076  primrootspoweq0  42079  aks6d1c2p2  42092  hashscontpow  42095  aks6d1c2lem4  42100  aks6d1c2  42103  aks6d1c5  42112  sticksstones8  42126  sticksstones12  42131  sticksstones22  42141  aks6d1c6lem3  42145  aks6d1c6isolem1  42147  unitscyglem3  42170  aks5  42177  sn-subeu  42400  sn-0tie0  42424  fiabv  42509  frlmsnic  42513  fsuppind  42563  prjspersym  42580  dffltz  42607  nna4b4nsq  42633  mzpindd  42719  mzpsubst  42721  mzpcompact2lem  42724  eldioph2b  42736  irrapxlem3  42797  irrapxlem5  42799  pellex  42808  pell1234qrdich  42834  pell14qrexpcl  42840  congabseq  42947  jm2.26a  42973  jm2.26lem3  42974  rmydioph  42987  lnrfg  43092  hbt  43103  cantnftermord  43293  cantnfresb  43297  cantnf2  43298  oawordex2  43299  omabs2  43305  tfsconcatfv  43314  tfsconcatrev  43321  ofoaass  43333  nadd2rabtr  43357  nadd1suc  43365  naddgeoa  43367  rfovcnvf1od  43977  clsk3nimkb  44013  ntrneiiso  44064  ntrneikb  44067  ntrneixb  44068  ntrneik3  44069  ntrneix3  44070  ntrneik13  44071  ntrneix13  44072  4an4132  44473  iunconnlem2  44908  modelaxrep  44955  fnchoice  45007  cncmpmax  45010  ssinc  45065  ssdec  45066  disjf1  45161  supxrge  45318  suplesup  45319  infxr  45347  infleinf  45352  unb2ltle  45395  rexabslelem  45398  uzub  45411  supminfxr  45444  climrec  45585  climsuse  45590  islptre  45601  addlimc  45630  0ellimcdiv  45631  limsuppnfdlem  45683  limsupub  45686  limsuppnflem  45692  limsupubuz  45695  climinf3  45698  limsupmnflem  45702  climxrre  45732  liminfreuzlem  45784  liminflimsupclim  45789  xlimliminflimsup  45844  icccncfext  45869  cncfiooicclem1  45875  fperdvper  45901  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvmptfprodlem  45926  dvmptfprod  45927  dvnprodlem2  45929  stoweidlem7  45989  stoweidlem34  46016  stoweidlem52  46034  stoweidlem60  46042  wallispilem3  46049  fourierdlem34  46123  fourierdlem38  46127  fourierdlem39  46128  fourierdlem48  46136  fourierdlem50  46138  fourierdlem51  46139  fourierdlem73  46161  fourierdlem76  46164  fourierdlem77  46165  fourierdlem80  46168  fourierdlem87  46175  fourierdlem103  46191  fourierdlem104  46192  etransclem32  46248  etransclem33  46249  sge0f1o  46364  sge0pr  46376  sge0isum  46409  iundjiun  46442  meaiininclem  46468  pimdecfgtioo  46699  pimincfltioo  46700  preimageiingt  46702  preimaleiinlt  46703  smflimlem2  46754  smflimlem4  46756  smfmullem3  46775  smflimmpt  46792  smfinflem  46799  smfpimne2  46822  fsupdm  46824  finfdm  46828  cfsetsnfsetfo  47045  funressnbrafv2  47229  imasetpreimafvbijlemf1  47389  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  bgoldbtbnd  47794  isuspgrim  47881  stgrusgra  47944  isubgr3stgrlem6  47956  2zlidl  48225  lindslinindsimp2  48449  snlindsntor  48457  lincresunit2  48464  islindeps2  48469  imaf1co  49141  imasubc3  49142  fucofvalg  49304  fuco21  49322  precofvalALT  49354  lanfval  49599  ranfval  49600