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  7223  soisoi  7268  f1o2ndf1  8058  fimaproj  8071  fprlem2  8237  tz7.49  8370  omabs  8572  cofon1  8593  naddssim  8606  omxpenlem  8998  fopwdom  9005  findcard3  9174  frfi  9176  finsschain  9250  marypha1lem  9324  wemappo  9442  wdomtr  9468  cantnfp1  9578  ttrcltr  9613  harcard  9878  numacn  9947  infunsdom1  10110  sornom  10175  ssfin4  10208  fin1a2lem11  10308  fin1a2lem13  10310  fpwwe2lem12  10540  pwfseq  10562  mulcmpblnr  10969  00id  11295  addrid  11300  cnegex  11301  negeu  11357  add20  11636  ltmul12a  11984  lediv12a  12022  cru  12124  qextltlem  13103  xleadd1a  13154  xmullem  13165  xlemul1a  13189  ixxss12  13267  ioodisj  13384  fvf1tp  13695  fsuppmapnn0fz  13905  seqf1o  13952  mulexpz  14011  leexp1a  14084  faclbnd  14199  swrdswrdlem  14613  abs3lem  15248  rexico  15263  cau3lem  15264  rlim3  15407  ello12  15425  lo1bdd2  15433  elo12  15436  rlimconst  15453  isercoll  15577  climcau  15580  climbdd  15581  summolem2  15625  fsumconst  15699  o1fsum  15722  incexclem  15745  fprodconst  15887  bitsfzo  16348  dvdsmulgcd  16469  pc2dvds  16793  pcz  16795  pcadd  16803  pcfac  16813  vdwmc2  16893  vdwlem2  16896  vdwlem10  16904  vdw  16908  ramcl  16943  sbcie3s  17075  firest  17338  prdsval  17361  mreexd  17550  mreexexlemd  17552  iscat  17580  cidfval  17584  iscatd2  17589  catcocl  17593  catass  17594  catpropd  17617  cidpropd  17618  moni  17645  monpropd  17646  issubc  17744  subccocl  17754  funcco  17780  funcpropd  17811  fullpropd  17831  nati  17867  natpropd  17888  fucpropd  17889  xpcpropd  18116  curfuncf  18146  curf2ndf  18155  yonffthlem  18190  acsfiindd  18461  chnind  18529  chnso  18532  mgmhmeql  18626  sgrppropd  18641  mndpropd  18669  mhmeql  18736  smndex1mgm  18817  isgrpinv  18908  dfgrp3lem  18953  mhmmnd  18979  cycsubm  19116  cycsubmcom  19118  conjnmzb  19167  ghmqusnsg  19196  ghmquskerlem3  19200  ghmqusker  19201  gass  19215  symgextf  19331  dfod2  19478  gexdvds  19498  sylow3lem2  19542  efgredlem  19661  efgredeu  19666  ghmcmn  19745  oddvdssubg  19769  dprdfcntz  19931  pgpfaclem3  19999  gsumle  20059  isrng  20074  issrg  20108  isring  20157  dvdsrmul1  20289  issubdrg  20697  suborng  20793  islmhm2  20974  lmhmeql  20991  lssacsex  21083  rhmpreimaidl  21216  rhmqusnsg  21224  isphl  21567  uvcf1  21731  lindfmm  21766  sraassab  21807  issubassa2  21831  opsrval  21982  psdmul  22082  scmatmats  22427  smatvscl  22440  mdetunilem7  22534  gsummatr01lem4  22574  m2cpmfo  22672  pmatcollpw3fi1lem1  22702  pm2mpf1lem  22710  pm2mpf1  22715  mp2pm2mplem4  22725  pm2mpghm  22732  chfacfscmulfsupp  22775  chfacfpmmulfsupp  22779  cctop  22922  neiptoptop  23047  neiptopreu  23049  tgrest  23075  ordtrest2lem  23119  cnss1  23192  cncnp  23196  isnrm3  23275  uncmp  23319  cmpfi  23324  iunconn  23344  1stcrest  23369  subislly  23397  islly2  23400  cldllycmp  23411  lly1stc  23412  llycmpkgen2  23466  kgencn  23472  xkoccn  23535  ptcnplem  23537  pthaus  23554  txhaus  23563  txkgen  23568  xkohaus  23569  xkococnlem  23575  txconn  23605  regr1lem2  23656  kqreglem1  23657  reghmph  23709  nrmhmph  23710  trfil2  23803  ufileu  23835  flimopn  23891  flimcf  23898  fclscf  23941  ufilcmp  23948  cnpfcf  23957  cnextfun  23980  tgpmulg  24009  symgtgp  24022  tgpt0  24035  qustgplem  24037  ustex2sym  24133  ustex3sym  24134  trust  24145  restutop  24153  restutopopn  24154  ustuqtop4  24160  utop3cls  24167  utopreg  24168  cstucnd  24199  ucncn  24200  trcfilu  24209  neipcfilu  24211  ismet2  24249  metequiv2  24426  metcnp  24457  metcnp2  24458  metcnpi3  24462  txmetcnp  24463  metustto  24469  metustsym  24471  metust  24474  cfilucfil  24475  metuel2  24481  psmetutop  24483  restmetu  24486  metucn  24487  ngptgp  24552  tngngp  24570  nmoleub  24647  icccmp  24742  reconnlem2  24744  reconn  24745  xmetdcn2  24754  metdseq0  24771  metdscn  24773  elcncf2  24811  cncfmet  24830  cnheibor  24882  nmoleub2lem2  25044  nmoleub3  25047  cvsi  25058  iscfil2  25194  iscfil3  25201  cfilfcls  25202  equivcfil  25227  caubl  25236  bcthlem5  25256  pmltpc  25379  ovollb2  25418  ovoliunnul  25436  ovolicc2lem4  25449  volsup  25485  ioorf  25502  dyadss  25523  dyaddisjlem  25524  mbfposr  25581  cncombf  25587  mbflimsup  25595  i1fmulclem  25631  mbfi1fseqlem4  25647  iblss2  25735  ellimc2  25806  ellimc3  25808  dvnadd  25859  dvmptfsum  25907  dvferm1  25917  dvferm2  25919  fta1g  26103  plyeq0lem  26143  plydivex  26233  fta1  26244  aalioulem2  26269  aalioulem3  26270  ulmuni  26329  ulmbdd  26335  ulmdvlem3  26339  mtest  26341  abelthlem8  26377  efopn  26595  cxpmul2z  26628  cxpcn3lem  26685  jensen  26927  lgambdd  26975  lgamucov  26976  isppw2  27053  mersenne  27166  dchrelbas3  27177  dchrptlem1  27203  dchrpt  27206  lgsval2lem  27246  lgsdchrval  27293  lgsquad3  27326  2sqb  27371  2sqmo  27376  pntrsumbnd2  27506  pntpbnd  27527  pntibnd  27532  nosupno  27643  noinfno  27658  noetasuplem4  27676  noetalem1  27681  madebday  27846  cofcutr  27869  negsprop  27978  mulscom  28079  absmuls  28183  zs12ge0  28394  remulscl  28405  tgjustr  28453  tglowdim1i  28480  tgbtwndiff  28485  tgifscgr  28487  iscgrglt  28493  tgcgrxfr  28497  lnext  28546  tgbtwnconn1lem3  28553  tgbtwnconn1  28554  legval  28563  legov  28564  legov2  28565  legtrd  28568  legtri3  28569  legso  28578  hlcgrex  28595  hlcgreu  28597  tglnne  28607  tglndim0  28608  tglineeltr  28610  tglinethru  28615  tglnne0  28619  tglnpt2  28620  colline  28628  tglowdim2l  28629  tglowdim2ln  28630  mirreu3  28633  miriso  28649  midexlem  28671  isperp  28691  perpcom  28692  perpneq  28693  isperp2  28694  footexALT  28697  footex  28700  colperpexlem3  28711  opphllem  28714  midex  28716  oppne3  28722  opptgdim2  28724  opphllem2  28727  opphllem3  28728  opphllem5  28730  opphllem6  28731  opphl  28733  outpasch  28734  lnopp2hpgb  28742  colopp  28748  lmieu  28763  trgcopy  28783  trgcopyeu  28785  iscgra1  28789  cgrane1  28791  cgrane2  28792  cgrane3  28793  cgrahl1  28795  cgrahl2  28796  cgracgr  28797  cgraswap  28799  cgracom  28801  cgratr  28802  flatcgra  28803  cgrabtwn  28805  cgrahl  28806  dfcgra2  28809  sacgr  28810  acopyeu  28813  inaghl  28824  cgrg3col4  28832  f1otrg  28850  f1otrge  28851  axsegcon  28907  axeuclidlem  28942  upgr1eopALT  29097  usgr1eop  29230  pthdepisspth  29715  wpthswwlks2on  29944  clwwlkf1  30031  clwwlknscsh  30044  2pthfrgr  30266  n4cyclfrgr  30273  frgrwopreglem5  30303  frgrwopreglem5ALT  30304  friendshipgt3  30380  smcnlem  30679  0lno  30772  ubthlem1  30852  ubthlem3  30854  chocunii  31283  occl  31286  5oalem1  31636  3oalem2  31645  nmopub2tALT  31891  nmfnleub2  31908  lnconi  32015  kbass5  32102  mdslmd1lem1  32307  mdslmd1lem2  32308  cdj1i  32415  opreu2reuALT  32458  disjabrex  32564  disjabrexf  32565  2ndresdju  32633  acunirnmpt  32643  acunirnmpt2  32644  acunirnmpt2f  32645  aciunf1lem  32646  fnpreimac  32655  fgreu  32656  suppovss  32666  xrge0infss  32747  xrofsup  32754  elq2  32799  fsumiunle  32817  sgnsub  32825  2exple2exp  32833  s3f1  32935  ccatf1  32937  ccatws1f1o  32939  swrdf1  32944  ressprs  32954  dfmgc2  32984  mgcf1o  32991  xrge0addgt0  33005  mndlrinvb  33013  mndlactf1  33014  mndlactfo  33015  mndractf1  33016  mndractfo  33017  mndlactf1o  33018  gsumfs2d  33042  gsumwun  33052  gsumwrd2dccatlem  33053  psgnfzto1stlem  33076  fzto1st1  33078  cycpmco2  33109  cycpmrn  33119  cyc3genpm  33128  cycpmconjs  33132  cyc3conja  33133  conjga  33146  fxpsubrg  33150  submarchi  33162  isarchi3  33163  archiabllem1  33169  archiabllem2a  33170  isarchiofld  33175  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem4  33219  elrgspnsubrunlem2  33222  erler  33239  rlocaddval  33242  rlocmulval  33243  rloccring  33244  rloc1r  33246  subrdom  33258  isdrng4  33268  fracfld  33281  imaslmod  33325  dvdsruasso  33357  unitprodclb  33361  nsgqusf1olem2  33386  lmhmqusker  33389  intlidl  33392  rhmquskerlem  33397  elrspunidl  33400  elrspunsn  33401  rhmimaidl  33404  prmidl2  33413  isprmidlc  33419  rhmpreimaprmidl  33423  qsidomlem2  33425  ssdifidllem  33428  ssdifidlprm  33430  mxidlprm  33442  ssmxidl  33446  opprqusplusg  33461  opprqusmulr  33463  qsdrngilem  33466  qsdrngi  33467  rsprprmprmidl  33494  rsprprmprmidlb  33495  rprmirred  33503  rprmirredb  33504  rprmdvdspow  33505  rprmdvdsprod  33506  1arithidom  33509  1arithufdlem2  33517  1arithufdlem3  33518  1arithufdlem4  33519  dfufd2lem  33521  dfufd2  33522  zringfrac  33526  ply1dg3rt0irred  33553  r1plmhm  33577  r1pquslmic  33578  extvfvcl  33587  mplmulmvr  33590  mplvrpmga  33593  esplyfval3  33612  esplyind  33613  exsslsb  33630  lindsunlem  33658  lindsun  33659  dimkerim  33661  fedgmullem1  33663  fedgmul  33665  dimlssid  33666  evls1fldgencl  33704  fldextrspunlsplem  33707  extdgfialg  33728  minplyirred  33745  fldext2chn  33762  constrmon  33778  constrconj  33779  constrfin  33780  constrelextdg2  33781  constrextdg2lem  33782  constrextdg2  33783  constrext2chnlem  33784  constrfiss  33785  cos9thpiminplylem2  33817  mdetpmtr1  33857  txomap  33868  qtophaus  33870  cmpcref  33884  zarclsun  33904  zarclssn  33907  zarcmplem  33915  pstmxmet  33931  sqsscirc1  33942  ordtrest2NEWlem  33956  ordtconnlem1  33958  pnfneige0  33985  lmxrge0  33986  lmdvg  33987  qqhval2  34016  esumcst  34097  esumrnmpt2  34102  esumfsup  34104  esumcvg  34120  esum2d  34127  esumiun  34128  sigaclfu2  34155  insiga  34171  ldsysgenld  34194  ldgenpisyslem1  34197  fiunelros  34208  measinb  34255  imambfm  34296  oms0  34331  omssubadd  34334  carsgclctunlem3  34354  eulerpartlemgvv  34410  dstrvprob  34506  signstfvneq0  34606  actfunsnrndisj  34639  reprinfz1  34656  breprexp  34667  afsval  34705  derangenlem  35236  sconnpi1  35304  cvmsss2  35339  cvmopnlem  35343  cvmlift3lem7  35390  msrval  35603  ifscgr  36109  cgrxfr  36120  btwnconn1lem13  36164  outsideofeu  36196  neibastop2lem  36425  weiunso  36531  irrdifflemf  37390  irrdiff  37391  matunitlindflem1  37676  matunitlindflem2  37677  poimirlem14  37694  poimirlem22  37702  poimirlem29  37709  broucube  37714  heicant  37715  mblfinlem1  37717  itg2addnclem  37731  ftc1cnnc  37752  ftc1anclem7  37759  sstotbnd2  37834  equivtotbnd  37838  isbnd3  37844  ssbnd  37848  totbndbnd  37849  cntotbnd  37856  heibor1lem  37869  rrncmslem  37892  lssats  39131  lsat0cv  39152  lkrlss  39214  lfl1dim  39240  lfl1dim2N  39241  lkrpssN  39282  hlhgt2  39508  3dim2  39587  2dim  39589  lplncvrlvol  39735  paddasslem11  39949  pmapjat1  39972  2polssN  40034  pclfinclN  40069  pexmidlem8N  40096  lhpexle1lem  40126  4atex  40195  ltrnid  40254  trlator0  40290  cdlemg2cex  40710  tendodi1  40903  tendodi2  40904  diblss  41289  dihopelvalcpre  41367  dihatexv  41457  mapdval4N  41751  fldhmf1  42203  mndmolinv  42208  primrootscoprmpow  42212  posbezout  42213  primrootscoprbij2  42216  primrootspoweq0  42219  aks6d1c2p2  42232  hashscontpow  42235  aks6d1c2lem4  42240  aks6d1c2  42243  aks6d1c5  42252  sticksstones8  42266  sticksstones12  42271  sticksstones22  42281  aks6d1c6lem3  42285  aks6d1c6isolem1  42287  unitscyglem3  42310  aks5  42317  sn-subeu  42545  sn-0tie0  42569  fiabv  42654  frlmsnic  42658  fsuppind  42708  prjspersym  42725  dffltz  42752  nna4b4nsq  42778  mzpindd  42863  mzpsubst  42865  mzpcompact2lem  42868  eldioph2b  42880  irrapxlem3  42941  irrapxlem5  42943  pellex  42952  pell1234qrdich  42978  pell14qrexpcl  42984  congabseq  43091  jm2.26a  43117  jm2.26lem3  43118  rmydioph  43131  lnrfg  43236  hbt  43247  cantnftermord  43437  cantnfresb  43441  cantnf2  43442  oawordex2  43443  omabs2  43449  tfsconcatfv  43458  tfsconcatrev  43465  ofoaass  43477  nadd2rabtr  43501  nadd1suc  43509  naddgeoa  43511  rfovcnvf1od  44121  clsk3nimkb  44157  ntrneiiso  44208  ntrneikb  44211  ntrneixb  44212  ntrneik3  44213  ntrneix3  44214  ntrneik13  44215  ntrneix13  44216  4an4132  44616  iunconnlem2  45051  modelaxrep  45098  fnchoice  45150  cncmpmax  45153  ssinc  45208  ssdec  45209  disjf1  45304  supxrge  45461  suplesup  45462  infxr  45489  infleinf  45494  unb2ltle  45537  rexabslelem  45540  uzub  45553  supminfxr  45586  climrec  45727  climsuse  45732  islptre  45743  addlimc  45770  0ellimcdiv  45771  limsuppnfdlem  45823  limsupub  45826  limsuppnflem  45832  limsupubuz  45835  climinf3  45838  limsupmnflem  45842  climxrre  45872  liminfreuzlem  45924  liminflimsupclim  45929  xlimliminflimsup  45984  icccncfext  46009  cncfiooicclem1  46015  fperdvper  46041  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvmptfprodlem  46066  dvmptfprod  46067  dvnprodlem2  46069  stoweidlem7  46129  stoweidlem34  46156  stoweidlem52  46174  stoweidlem60  46182  wallispilem3  46189  fourierdlem34  46263  fourierdlem38  46267  fourierdlem39  46268  fourierdlem48  46276  fourierdlem50  46278  fourierdlem51  46279  fourierdlem73  46301  fourierdlem76  46304  fourierdlem77  46305  fourierdlem80  46308  fourierdlem87  46315  fourierdlem103  46331  fourierdlem104  46332  etransclem32  46388  etransclem33  46389  sge0f1o  46504  sge0pr  46516  sge0isum  46549  iundjiun  46582  meaiininclem  46608  pimdecfgtioo  46839  pimincfltioo  46840  preimageiingt  46842  preimaleiinlt  46843  smflimlem2  46894  smflimlem4  46896  smfmullem3  46915  smflimmpt  46932  smfinflem  46939  smfpimne2  46962  fsupdm  46964  finfdm  46968  cfsetsnfsetfo  47184  funressnbrafv2  47368  imasetpreimafvbijlemf1  47528  bgoldbtbndlem2  47930  bgoldbtbndlem3  47931  bgoldbtbnd  47933  isuspgrim  48020  stgrusgra  48083  isubgr3stgrlem6  48095  2zlidl  48364  lindslinindsimp2  48588  snlindsntor  48596  lincresunit2  48603  islindeps2  48608  imaf1co  49280  imasubc3  49281  fucofvalg  49443  fuco21  49461  precofvalALT  49493  lanfval  49738  ranfval  49739