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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  frpomin  6342  fsnex  7281  soisoi  7325  f1o2ndf1  8108  fimaproj  8121  fprlem2  8286  tz7.49  8445  omabs  8650  cofon1  8671  naddssim  8684  omxpenlem  9073  fopwdom  9080  findcard3  9285  findcard3OLD  9286  frfi  9288  finsschain  9359  marypha1lem  9428  wemappo  9544  wdomtr  9570  cantnfp1  9676  ttrcltr  9711  harcard  9973  numacn  10044  infunsdom1  10208  sornom  10272  ssfin4  10305  fin1a2lem11  10405  fin1a2lem13  10407  fpwwe2lem12  10637  pwfseq  10659  mulcmpblnr  11066  00id  11389  addrid  11394  cnegex  11395  negeu  11450  add20  11726  ltmul12a  12070  lediv12a  12107  cru  12204  qextltlem  13181  xleadd1a  13232  xmullem  13243  xlemul1a  13267  ixxss12  13344  ioodisj  13459  fsuppmapnn0fz  13961  seqf1o  14009  mulexpz  14068  leexp1a  14140  faclbnd  14250  swrdswrdlem  14654  abs3lem  15285  rexico  15300  cau3lem  15301  rlim3  15442  ello12  15460  lo1bdd2  15468  elo12  15471  rlimconst  15488  isercoll  15614  climcau  15617  climbdd  15618  summolem2  15662  fsumconst  15736  o1fsum  15759  incexclem  15782  fprodconst  15922  bitsfzo  16376  dvdsmulgcd  16497  pc2dvds  16812  pcz  16814  pcadd  16822  pcfac  16832  vdwmc2  16912  vdwlem2  16915  vdwlem10  16923  vdw  16927  ramcl  16962  sbcie3s  17095  firest  17378  prdsval  17401  mreexd  17586  mreexexlemd  17588  iscat  17616  cidfval  17620  iscatd2  17625  catcocl  17629  catass  17630  catpropd  17653  cidpropd  17654  moni  17683  monpropd  17684  issubc  17785  subccocl  17795  funcco  17821  funcpropd  17851  fullpropd  17871  nati  17906  natpropd  17929  fucpropd  17930  xpcpropd  18161  curfuncf  18191  curf2ndf  18200  yonffthlem  18235  acsfiindd  18506  sgrppropd  18622  mndpropd  18650  mhmeql  18707  smndex1mgm  18788  isgrpinv  18878  dfgrp3lem  18921  mhmmnd  18947  cycsubm  19079  cycsubmcom  19081  conjnmzb  19127  gass  19165  symgextf  19285  dfod2  19432  gexdvds  19452  sylow3lem2  19496  efgredlem  19615  efgredeu  19620  ghmcmn  19699  oddvdssubg  19723  dprdfcntz  19885  pgpfaclem3  19953  issrg  20011  isring  20060  dvdsrmul1  20183  issubdrg  20401  islmhm2  20649  lmhmeql  20666  lssacsex  20757  isphl  21181  uvcf1  21347  lindfmm  21382  sraassab  21422  issubassa2  21446  opsrval  21601  mhpmulcl  21692  scmatmats  22013  smatvscl  22026  mdetunilem7  22120  gsummatr01lem4  22160  m2cpmfo  22258  pmatcollpw3fi1lem1  22288  pm2mpf1lem  22296  pm2mpf1  22301  mp2pm2mplem4  22311  pm2mpghm  22318  chfacfscmulfsupp  22361  chfacfpmmulfsupp  22365  cctop  22509  neiptoptop  22635  neiptopreu  22637  tgrest  22663  ordtrest2lem  22707  cnss1  22780  cncnp  22784  isnrm3  22863  uncmp  22907  cmpfi  22912  iunconn  22932  1stcrest  22957  subislly  22985  islly2  22988  cldllycmp  22999  lly1stc  23000  llycmpkgen2  23054  kgencn  23060  xkoccn  23123  ptcnplem  23125  pthaus  23142  txhaus  23151  txkgen  23156  xkohaus  23157  xkococnlem  23163  txconn  23193  regr1lem2  23244  kqreglem1  23245  reghmph  23297  nrmhmph  23298  trfil2  23391  ufileu  23423  flimopn  23479  flimcf  23486  fclscf  23529  ufilcmp  23536  cnpfcf  23545  cnextfun  23568  tgpmulg  23597  symgtgp  23610  tgpt0  23623  qustgplem  23625  ustex2sym  23721  ustex3sym  23722  trust  23734  restutop  23742  restutopopn  23743  ustuqtop4  23749  utop3cls  23756  utopreg  23757  cstucnd  23789  ucncn  23790  trcfilu  23799  neipcfilu  23801  ismet2  23839  metequiv2  24019  metcnp  24050  metcnp2  24051  metcnpi3  24055  txmetcnp  24056  metustto  24062  metustsym  24064  metust  24067  cfilucfil  24068  metuel2  24074  psmetutop  24076  restmetu  24079  metucn  24080  ngptgp  24145  tngngp  24171  nmoleub  24248  icccmp  24341  reconnlem2  24343  reconn  24344  xmetdcn2  24353  metdseq0  24370  metdscn  24372  elcncf2  24406  cncfmet  24425  cnheibor  24471  nmoleub2lem2  24632  nmoleub3  24635  cvsi  24646  iscfil2  24783  iscfil3  24790  cfilfcls  24791  equivcfil  24816  caubl  24825  bcthlem5  24845  pmltpc  24967  ovollb2  25006  ovoliunnul  25024  ovolicc2lem4  25037  volsup  25073  ioorf  25090  dyadss  25111  dyaddisjlem  25112  mbfposr  25169  cncombf  25175  mbflimsup  25183  i1fmulclem  25220  mbfi1fseqlem4  25236  iblss2  25323  ellimc2  25394  ellimc3  25396  dvnadd  25446  dvmptfsum  25492  dvferm1  25502  dvferm2  25504  fta1g  25685  plyeq0lem  25724  plydivex  25810  fta1  25821  aalioulem2  25846  aalioulem3  25847  ulmuni  25904  ulmbdd  25910  ulmdvlem3  25914  mtest  25916  abelthlem8  25951  efopn  26166  cxpmul2z  26199  cxpcn3lem  26255  jensen  26493  lgambdd  26541  lgamucov  26542  isppw2  26619  mersenne  26730  dchrelbas3  26741  dchrptlem1  26767  dchrpt  26770  lgsval2lem  26810  lgsdchrval  26857  lgsquad3  26890  2sqb  26935  2sqmo  26940  pntrsumbnd2  27070  pntpbnd  27091  pntibnd  27096  nosupno  27206  noinfno  27221  noetasuplem4  27239  noetalem1  27244  madebday  27395  cofcutr  27413  negsprop  27512  mulscom  27598  tgjustr  27756  tglowdim1i  27783  tgbtwndiff  27788  tgifscgr  27790  iscgrglt  27796  tgcgrxfr  27800  lnext  27849  tgbtwnconn1lem3  27856  tgbtwnconn1  27857  legval  27866  legov  27867  legov2  27868  legtrd  27871  legtri3  27872  legso  27881  hlcgrex  27898  hlcgreu  27900  tglnne  27910  tglndim0  27911  tglineeltr  27913  tglinethru  27918  tglnne0  27922  tglnpt2  27923  colline  27931  tglowdim2l  27932  tglowdim2ln  27933  mirreu3  27936  miriso  27952  midexlem  27974  isperp  27994  perpcom  27995  perpneq  27996  isperp2  27997  footexALT  28000  footex  28003  colperpexlem3  28014  opphllem  28017  midex  28019  oppne3  28025  opptgdim2  28027  opphllem2  28030  opphllem3  28031  opphllem5  28033  opphllem6  28034  opphl  28036  outpasch  28037  lnopp2hpgb  28045  colopp  28051  lmieu  28066  trgcopy  28086  trgcopyeu  28088  iscgra1  28092  cgrane1  28094  cgrane2  28095  cgrane3  28096  cgrahl1  28098  cgrahl2  28099  cgracgr  28100  cgraswap  28102  cgracom  28104  cgratr  28105  flatcgra  28106  cgrabtwn  28108  cgrahl  28109  dfcgra2  28112  sacgr  28113  acopyeu  28116  inaghl  28127  cgrg3col4  28135  f1otrg  28153  f1otrge  28154  axsegcon  28216  axeuclidlem  28251  upgr1eopALT  28408  usgr1eop  28538  pthdepisspth  29023  wpthswwlks2on  29246  clwwlkf1  29333  clwwlknscsh  29346  2pthfrgr  29568  n4cyclfrgr  29575  frgrwopreglem5  29605  frgrwopreglem5ALT  29606  friendshipgt3  29682  smcnlem  29981  0lno  30074  ubthlem1  30154  ubthlem3  30156  chocunii  30585  occl  30588  5oalem1  30938  3oalem2  30947  nmopub2tALT  31193  nmfnleub2  31210  lnconi  31317  kbass5  31404  mdslmd1lem1  31609  mdslmd1lem2  31610  cdj1i  31717  opreu2reuALT  31748  disjabrex  31844  disjabrexf  31845  2ndresdju  31905  acunirnmpt  31915  acunirnmpt2  31916  acunirnmpt2f  31917  aciunf1lem  31918  fnpreimac  31927  fgreu  31928  suppovss  31937  xrge0infss  32004  xrofsup  32011  fsumiunle  32066  s3f1  32144  ccatf1  32146  swrdf1  32151  ressprs  32164  dfmgc2  32197  mgcf1o  32204  xrge0addgt0  32223  gsumle  32273  psgnfzto1stlem  32290  fzto1st1  32292  cycpmco2  32323  cycpmrn  32333  cyc3genpm  32342  cycpmconjs  32346  cyc3conja  32347  submarchi  32363  isarchi3  32364  archiabllem1  32370  archiabllem2a  32371  isdrng4  32426  suborng  32464  isarchiofld  32466  imaslmod  32499  dvdsruasso  32521  nsgqusf1olem2  32556  ghmquskerlem3  32562  ghmqusker  32563  lmhmqusker  32565  intlidl  32567  rhmpreimaidl  32568  rhmquskerlem  32574  elrspunidl  32577  elrspunsn  32578  rhmimaidl  32581  prmidl2  32590  isprmidlc  32597  rhmpreimaprmidl  32601  qsidomlem2  32603  mxidlprm  32617  ssmxidl  32621  opprqusplusg  32634  opprqusmulr  32636  qsdrngilem  32639  qsdrngi  32640  lindsunlem  32740  lindsun  32741  dimkerim  32743  fedgmullem1  32745  fedgmul  32747  minplyirred  32801  mdetpmtr1  32834  txomap  32845  qtophaus  32847  cmpcref  32861  zarclsun  32881  zarclssn  32884  zarcmplem  32892  pstmxmet  32908  sqsscirc1  32919  ordtrest2NEWlem  32933  ordtconnlem1  32935  pnfneige0  32962  lmxrge0  32963  lmdvg  32964  qqhval2  32993  esumcst  33092  esumrnmpt2  33097  esumfsup  33099  esumcvg  33115  esum2d  33122  esumiun  33123  sigaclfu2  33150  insiga  33166  ldsysgenld  33189  ldgenpisyslem1  33192  fiunelros  33203  measinb  33250  imambfm  33292  oms0  33327  omssubadd  33330  carsgclctunlem3  33350  eulerpartlemgvv  33406  dstrvprob  33501  sgnsub  33574  signstfvneq0  33614  actfunsnrndisj  33648  reprinfz1  33665  breprexp  33676  afsval  33714  derangenlem  34193  sconnpi1  34261  cvmsss2  34296  cvmopnlem  34300  cvmlift3lem7  34347  msrval  34560  ifscgr  35047  cgrxfr  35058  btwnconn1lem13  35102  outsideofeu  35134  neibastop2lem  35293  irrdifflemf  36254  irrdiff  36255  matunitlindflem1  36532  matunitlindflem2  36533  poimirlem14  36550  poimirlem22  36558  poimirlem29  36565  broucube  36570  heicant  36571  mblfinlem1  36573  itg2addnclem  36587  ftc1cnnc  36608  ftc1anclem7  36615  sstotbnd2  36690  equivtotbnd  36694  isbnd3  36700  ssbnd  36704  totbndbnd  36705  cntotbnd  36712  heibor1lem  36725  rrncmslem  36748  lssats  37930  lsat0cv  37951  lkrlss  38013  lfl1dim  38039  lfl1dim2N  38040  lkrpssN  38081  hlhgt2  38308  3dim2  38387  2dim  38389  lplncvrlvol  38535  paddasslem11  38749  pmapjat1  38772  2polssN  38834  pclfinclN  38869  pexmidlem8N  38896  lhpexle1lem  38926  4atex  38995  ltrnid  39054  trlator0  39090  cdlemg2cex  39510  tendodi1  39703  tendodi2  39704  diblss  40089  dihopelvalcpre  40167  dihatexv  40257  mapdval4N  40551  fldhmf1  41003  aks6d1c2p2  41005  sticksstones8  41017  sticksstones12  41022  sticksstones22  41032  metakunt1  41033  metakunt2  41034  frlmsnic  41158  fsuppind  41210  sn-subeu  41347  sn-0tie0  41360  prjspersym  41397  dffltz  41424  nna4b4nsq  41450  mzpindd  41532  mzpsubst  41534  mzpcompact2lem  41537  eldioph2b  41549  irrapxlem3  41610  irrapxlem5  41612  pellex  41621  pell1234qrdich  41647  pell14qrexpcl  41653  congabseq  41761  jm2.26a  41787  jm2.26lem3  41788  rmydioph  41801  lnrfg  41909  hbt  41920  cantnftermord  42118  cantnfresb  42122  cantnf2  42123  oawordex2  42124  omabs2  42130  tfsconcatfv  42139  tfsconcatrev  42146  ofoaass  42158  nadd2rabtr  42182  nadd1suc  42190  naddgeoa  42193  rfovcnvf1od  42803  clsk3nimkb  42839  ntrneiiso  42890  ntrneikb  42893  ntrneixb  42894  ntrneik3  42895  ntrneix3  42896  ntrneik13  42897  ntrneix13  42898  4an4132  43308  iunconnlem2  43744  fnchoice  43761  cncmpmax  43764  ssinc  43824  ssdec  43825  disjf1  43928  supxrge  44096  suplesup  44097  infxr  44125  infleinf  44130  unb2ltle  44173  rexabslelem  44176  uzub  44189  supminfxr  44222  climrec  44367  climsuse  44372  islptre  44383  addlimc  44412  0ellimcdiv  44413  limsuppnfdlem  44465  limsupub  44468  limsuppnflem  44474  limsupubuz  44477  climinf3  44480  limsupmnflem  44484  climxrre  44514  liminfreuzlem  44566  liminflimsupclim  44571  xlimliminflimsup  44626  icccncfext  44651  cncfiooicclem1  44657  fperdvper  44683  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  dvmptfprodlem  44708  dvmptfprod  44709  dvnprodlem2  44711  stoweidlem7  44771  stoweidlem34  44798  stoweidlem52  44816  stoweidlem60  44824  wallispilem3  44831  fourierdlem34  44905  fourierdlem38  44909  fourierdlem39  44910  fourierdlem48  44918  fourierdlem50  44920  fourierdlem51  44921  fourierdlem73  44943  fourierdlem76  44946  fourierdlem77  44947  fourierdlem80  44950  fourierdlem87  44957  fourierdlem103  44973  fourierdlem104  44974  etransclem32  45030  etransclem33  45031  sge0f1o  45146  sge0pr  45158  sge0isum  45191  iundjiun  45224  meaiininclem  45250  pimdecfgtioo  45481  pimincfltioo  45482  preimageiingt  45484  preimaleiinlt  45485  smflimlem2  45536  smflimlem4  45538  smfmullem3  45557  smflimmpt  45574  smfinflem  45581  smfpimne2  45604  fsupdm  45606  finfdm  45610  cfsetsnfsetfo  45818  funressnbrafv2  46000  imasetpreimafvbijlemf1  46120  bgoldbtbndlem2  46522  bgoldbtbndlem3  46523  bgoldbtbnd  46525  isomuspgrlem2  46549  mgmhmeql  46621  isrng  46698  2zlidl  46880  lindslinindsimp2  47192  snlindsntor  47200  lincresunit2  47207  islindeps2  47212