Theorem simpllr 773

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  frpomin  6247  fsnex  7164  soisoi  7208  f1o2ndf1  7972  fimaproj  7985  fprlem2  8126  tz7.49  8285  omabs  8490  omxpenlem  8869  fopwdom  8876  findcard3  9066  frfi  9068  finsschain  9135  marypha1lem  9201  wemappo  9317  wdomtr  9343  cantnfp1  9448  ttrcltr  9483  harcard  9745  numacn  9814  infunsdom1  9978  sornom  10042  ssfin4  10075  fin1a2lem11  10175  fin1a2lem13  10177  fpwwe2lem12  10407  pwfseq  10429  mulcmpblnr  10836  00id  11159  addid1  11164  cnegex  11165  negeu  11220  add20  11496  ltmul12a  11840  lediv12a  11877  cru  11974  qextltlem  12945  xleadd1a  12996  xmullem  13007  xlemul1a  13031  ixxss12  13108  ioodisj  13223  fsuppmapnn0fz  13725  seqf1o  13773  mulexpz  13832  leexp1a  13902  faclbnd  14013  swrdswrdlem  14426  abs3lem  15059  rexico  15074  cau3lem  15075  rlim3  15216  ello12  15234  lo1bdd2  15242  elo12  15245  rlimconst  15262  isercoll  15388  climcau  15391  climbdd  15392  summolem2  15437  fsumconst  15511  o1fsum  15534  incexclem  15557  fprodconst  15697  bitsfzo  16151  dvdsmulgcd  16274  pc2dvds  16589  pcz  16591  pcadd  16599  pcfac  16609  vdwmc2  16689  vdwlem2  16692  vdwlem10  16700  vdw  16704  ramcl  16739  sbcie3s  16872  firest  17152  prdsval  17175  mreexd  17360  mreexexlemd  17362  iscat  17390  cidfval  17394  iscatd2  17399  catcocl  17403  catass  17404  catpropd  17427  cidpropd  17428  moni  17457  monpropd  17458  issubc  17559  subccocl  17569  funcco  17595  funcpropd  17625  fullpropd  17645  nati  17680  natpropd  17703  fucpropd  17704  xpcpropd  17935  curfuncf  17965  curf2ndf  17974  yonffthlem  18009  acsfiindd  18280  mndpropd  18419  mhmeql  18473  smndex1mgm  18555  isgrpinv  18641  dfgrp3lem  18682  mhmmnd  18706  cycsubm  18830  cycsubmcom  18832  conjnmzb  18878  gass  18916  symgextf  19034  dfod2  19180  gexdvds  19198  sylow3lem2  19242  efgredlem  19362  efgredeu  19367  ghmcmn  19442  oddvdssubg  19465  dprdfcntz  19627  pgpfaclem3  19695  issrg  19752  isring  19796  dvdsrmul1  19904  issubdrg  20058  islmhm2  20309  lmhmeql  20326  lssacsex  20415  isphl  20842  uvcf1  21008  lindfmm  21043  issubassa2  21105  opsrval  21256  mhpmulcl  21348  scmatmats  21669  smatvscl  21682  mdetunilem7  21776  gsummatr01lem4  21816  m2cpmfo  21914  pmatcollpw3fi1lem1  21944  pm2mpf1lem  21952  pm2mpf1  21957  mp2pm2mplem4  21967  pm2mpghm  21974  chfacfscmulfsupp  22017  chfacfpmmulfsupp  22021  cctop  22165  neiptoptop  22291  neiptopreu  22293  tgrest  22319  ordtrest2lem  22363  cnss1  22436  cncnp  22440  isnrm3  22519  uncmp  22563  cmpfi  22568  iunconn  22588  1stcrest  22613  subislly  22641  islly2  22644  cldllycmp  22655  lly1stc  22656  llycmpkgen2  22710  kgencn  22716  xkoccn  22779  ptcnplem  22781  pthaus  22798  txhaus  22807  txkgen  22812  xkohaus  22813  xkococnlem  22819  txconn  22849  regr1lem2  22900  kqreglem1  22901  reghmph  22953  nrmhmph  22954  trfil2  23047  ufileu  23079  flimopn  23135  flimcf  23142  fclscf  23185  ufilcmp  23192  cnpfcf  23201  cnextfun  23224  tgpmulg  23253  symgtgp  23266  tgpt0  23279  qustgplem  23281  ustex2sym  23377  ustex3sym  23378  trust  23390  restutop  23398  restutopopn  23399  ustuqtop4  23405  utop3cls  23412  utopreg  23413  cstucnd  23445  ucncn  23446  trcfilu  23455  neipcfilu  23457  ismet2  23495  metequiv2  23675  metcnp  23706  metcnp2  23707  metcnpi3  23711  txmetcnp  23712  metustto  23718  metustsym  23720  metust  23723  cfilucfil  23724  metuel2  23730  psmetutop  23732  restmetu  23735  metucn  23736  ngptgp  23801  tngngp  23827  nmoleub  23904  icccmp  23997  reconnlem2  23999  reconn  24000  xmetdcn2  24009  metdseq0  24026  metdscn  24028  elcncf2  24062  cncfmet  24081  cnheibor  24127  nmoleub2lem2  24288  nmoleub3  24291  cvsi  24302  iscfil2  24439  iscfil3  24446  cfilfcls  24447  equivcfil  24472  caubl  24481  bcthlem5  24501  pmltpc  24623  ovollb2  24662  ovoliunnul  24680  ovolicc2lem4  24693  volsup  24729  ioorf  24746  dyadss  24767  dyaddisjlem  24768  mbfposr  24825  cncombf  24831  mbflimsup  24839  i1fmulclem  24876  mbfi1fseqlem4  24892  iblss2  24979  ellimc2  25050  ellimc3  25052  dvnadd  25102  dvmptfsum  25148  dvferm1  25158  dvferm2  25160  fta1g  25341  plyeq0lem  25380  plydivex  25466  fta1  25477  aalioulem2  25502  aalioulem3  25503  ulmuni  25560  ulmbdd  25566  ulmdvlem3  25570  mtest  25572  abelthlem8  25607  efopn  25822  cxpmul2z  25855  cxpcn3lem  25909  jensen  26147  lgambdd  26195  lgamucov  26196  isppw2  26273  mersenne  26384  dchrelbas3  26395  dchrptlem1  26421  dchrpt  26424  lgsval2lem  26464  lgsdchrval  26511  lgsquad3  26544  2sqb  26589  2sqmo  26594  pntrsumbnd2  26724  pntpbnd  26745  pntibnd  26750  istrkgc  26824  istrkgb  26825  tgjustr  26844  tglowdim1i  26871  tgbtwndiff  26876  tgifscgr  26878  iscgrglt  26884  tgcgrxfr  26888  lnext  26937  tgbtwnconn1lem3  26944  tgbtwnconn1  26945  legval  26954  legov  26955  legov2  26956  legtrd  26959  legtri3  26960  legso  26969  hlcgrex  26986  hlcgreu  26988  tglnne  26998  tglndim0  26999  tglineeltr  27001  tglinethru  27006  tglnne0  27010  tglnpt2  27011  colline  27019  tglowdim2l  27020  tglowdim2ln  27021  mirreu3  27024  miriso  27040  midexlem  27062  isperp  27082  perpcom  27083  perpneq  27084  isperp2  27085  footexALT  27088  footex  27091  colperpexlem3  27102  opphllem  27105  midex  27107  oppne3  27113  opptgdim2  27115  opphllem2  27118  opphllem3  27119  opphllem5  27121  opphllem6  27122  opphl  27124  outpasch  27125  lnopp2hpgb  27133  colopp  27139  lmieu  27154  trgcopy  27174  trgcopyeu  27176  iscgra1  27180  cgrane1  27182  cgrane2  27183  cgrane3  27184  cgrahl1  27186  cgrahl2  27187  cgracgr  27188  cgraswap  27190  cgracom  27192  cgratr  27193  flatcgra  27194  cgrabtwn  27196  cgrahl  27197  dfcgra2  27200  sacgr  27201  acopyeu  27204  inaghl  27215  cgrg3col4  27223  f1otrg  27241  f1otrge  27242  axsegcon  27304  axeuclidlem  27339  upgr1eopALT  27496  usgr1eop  27626  pthdepisspth  28112  wpthswwlks2on  28335  clwwlkf1  28422  clwwlknscsh  28435  2pthfrgr  28657  n4cyclfrgr  28664  frgrwopreglem5  28694  frgrwopreglem5ALT  28695  friendshipgt3  28771  smcnlem  29068  0lno  29161  ubthlem1  29241  ubthlem3  29243  chocunii  29672  occl  29675  5oalem1  30025  3oalem2  30034  nmopub2tALT  30280  nmfnleub2  30297  lnconi  30404  kbass5  30491  mdslmd1lem1  30696  mdslmd1lem2  30697  cdj1i  30804  opreu2reuALT  30834  disjabrex  30930  disjabrexf  30931  2ndresdju  30995  acunirnmpt  31005  acunirnmpt2  31006  acunirnmpt2f  31007  aciunf1lem  31008  fnpreimac  31017  fgreu  31018  suppovss  31026  xrge0infss  31092  xrofsup  31099  fsumiunle  31152  s3f1  31230  ccatf1  31232  swrdf1  31237  ressprs  31250  dfmgc2  31283  mgcf1o  31290  xrge0addgt0  31309  gsumle  31359  psgnfzto1stlem  31376  fzto1st1  31378  cycpmco2  31409  cycpmrn  31419  cyc3genpm  31428  cycpmconjs  31432  cyc3conja  31433  submarchi  31449  isarchi3  31450  archiabllem1  31456  archiabllem2a  31457  suborng  31523  isarchiofld  31525  imaslmod  31562  nsgqusf1olem2  31608  intlidl  31611  rhmpreimaidl  31612  elrspunidl  31615  rhmimaidl  31618  prmidl2  31625  isprmidlc  31632  rhmpreimaprmidl  31636  qsidomlem2  31638  mxidlprm  31649  ssmxidl  31651  lindsunlem  31714  lindsun  31715  dimkerim  31717  fedgmullem1  31719  fedgmul  31721  mdetpmtr1  31782  txomap  31793  qtophaus  31795  cmpcref  31809  zarclsun  31829  zarclssn  31832  zarcmplem  31840  pstmxmet  31856  sqsscirc1  31867  ordtrest2NEWlem  31881  ordtconnlem1  31883  pnfneige0  31910  lmxrge0  31911  lmdvg  31912  qqhval2  31941  esumcst  32040  esumrnmpt2  32045  esumfsup  32047  esumcvg  32063  esum2d  32070  esumiun  32071  sigaclfu2  32098  insiga  32114  ldsysgenld  32137  ldgenpisyslem1  32140  fiunelros  32151  measinb  32198  imambfm  32238  oms0  32273  omssubadd  32276  carsgclctunlem3  32296  eulerpartlemgvv  32352  dstrvprob  32447  sgnsub  32520  signstfvneq0  32560  actfunsnrndisj  32594  reprinfz1  32611  breprexp  32622  afsval  32660  derangenlem  33142  sconnpi1  33210  cvmsss2  33245  cvmopnlem  33249  cvmlift3lem7  33296  msrval  33509  naddssim  33846  nosupno  33915  noinfno  33930  noetasuplem4  33948  noetalem1  33953  madebday  34089  cofcutr  34101  ifscgr  34355  cgrxfr  34366  btwnconn1lem13  34410  outsideofeu  34442  neibastop2lem  34558  irrdifflemf  35505  irrdiff  35506  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem14  35800  poimirlem22  35808  poimirlem29  35815  broucube  35820  heicant  35821  mblfinlem1  35823  itg2addnclem  35837  ftc1cnnc  35858  ftc1anclem7  35865  sstotbnd2  35941  equivtotbnd  35945  isbnd3  35951  ssbnd  35955  totbndbnd  35956  cntotbnd  35963  heibor1lem  35976  rrncmslem  35999  lssats  37033  lsat0cv  37054  lkrlss  37116  lfl1dim  37142  lfl1dim2N  37143  lkrpssN  37184  hlhgt2  37410  3dim2  37489  2dim  37491  lplncvrlvol  37637  paddasslem11  37851  pmapjat1  37874  2polssN  37936  pclfinclN  37971  pexmidlem8N  37998  lhpexle1lem  38028  4atex  38097  ltrnid  38156  trlator0  38192  cdlemg2cex  38612  tendodi1  38805  tendodi2  38806  diblss  39191  dihopelvalcpre  39269  dihatexv  39359  mapdval4N  39653  sticksstones8  40116  sticksstones12  40121  sticksstones22  40131  metakunt1  40132  metakunt2  40133  frlmsnic  40270  fsuppind  40286  sn-subeu  40415  sn-0tie0  40428  prjspersym  40453  dffltz  40478  nna4b4nsq  40504  mzpindd  40575  mzpsubst  40577  mzpcompact2lem  40580  eldioph2b  40592  irrapxlem3  40653  irrapxlem5  40655  pellex  40664  pell1234qrdich  40690  pell14qrexpcl  40696  congabseq  40803  jm2.26a  40829  jm2.26lem3  40830  rmydioph  40843  lnrfg  40951  hbt  40962  rfovcnvf1od  41619  clsk3nimkb  41657  ntrneiiso  41708  ntrneikb  41711  ntrneixb  41712  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  4an4132  42126  iunconnlem2  42562  fnchoice  42579  cncmpmax  42582  ssinc  42644  ssdec  42645  disjf1  42727  supxrge  42884  suplesup  42885  infxr  42913  infleinf  42918  unb2ltle  42962  rexabslelem  42965  uzub  42978  supminfxr  43011  climrec  43151  climsuse  43156  islptre  43167  addlimc  43196  0ellimcdiv  43197  limsuppnfdlem  43249  limsupub  43252  limsuppnflem  43258  limsupubuz  43261  climinf3  43264  limsupmnflem  43268  climxrre  43298  liminfreuzlem  43350  liminflimsupclim  43355  xlimliminflimsup  43410  icccncfext  43435  cncfiooicclem1  43441  fperdvper  43467  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvmptfprodlem  43492  dvmptfprod  43493  dvnprodlem2  43495  stoweidlem7  43555  stoweidlem34  43582  stoweidlem52  43600  stoweidlem60  43608  wallispilem3  43615  fourierdlem34  43689  fourierdlem38  43693  fourierdlem39  43694  fourierdlem48  43702  fourierdlem50  43704  fourierdlem51  43705  fourierdlem73  43727  fourierdlem76  43730  fourierdlem77  43731  fourierdlem80  43734  fourierdlem87  43741  fourierdlem103  43757  fourierdlem104  43758  etransclem32  43814  etransclem33  43815  sge0f1o  43927  sge0pr  43939  sge0isum  43972  iundjiun  44005  meaiininclem  44031  pimdecfgtioo  44262  pimincfltioo  44263  preimageiingt  44265  preimaleiinlt  44266  smflimlem2  44317  smflimlem4  44319  smfmullem3  44338  smflimmpt  44354  smfinflem  44361  cfsetsnfsetfo  44565  funressnbrafv2  44747  imasetpreimafvbijlemf1  44867  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbnd  45272  isomuspgrlem2  45296  mgmhmeql  45368  isrng  45445  2zlidl  45503  lindslinindsimp2  45815  snlindsntor  45823  lincresunit2  45830  islindeps2  45835