Theorem simpllr 772

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 727	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 206  df-an 396

This theorem is referenced by:  frpomin  6228  fsnex  7135  soisoi  7179  f1o2ndf1  7934  fimaproj  7947  fprlem2  8088  tz7.49  8246  omabs  8441  omxpenlem  8813  fopwdom  8820  findcard3  8987  frfi  8989  finsschain  9056  marypha1lem  9122  wemappo  9238  wdomtr  9264  cantnfp1  9369  frrlem16  9447  harcard  9667  numacn  9736  infunsdom1  9900  sornom  9964  ssfin4  9997  fin1a2lem11  10097  fin1a2lem13  10099  fpwwe2lem12  10329  pwfseq  10351  mulcmpblnr  10758  00id  11080  addid1  11085  cnegex  11086  negeu  11141  add20  11417  ltmul12a  11761  lediv12a  11798  cru  11895  qextltlem  12865  xleadd1a  12916  xmullem  12927  xlemul1a  12951  ixxss12  13028  ioodisj  13143  fsuppmapnn0fz  13644  seqf1o  13692  mulexpz  13751  leexp1a  13821  faclbnd  13932  swrdswrdlem  14345  abs3lem  14978  rexico  14993  cau3lem  14994  rlim3  15135  ello12  15153  lo1bdd2  15161  elo12  15164  rlimconst  15181  isercoll  15307  climcau  15310  climbdd  15311  summolem2  15356  fsumconst  15430  o1fsum  15453  incexclem  15476  fprodconst  15616  bitsfzo  16070  dvdsmulgcd  16193  pc2dvds  16508  pcz  16510  pcadd  16518  pcfac  16528  vdwmc2  16608  vdwlem2  16611  vdwlem10  16619  vdw  16623  ramcl  16658  sbcie3s  16791  firest  17060  prdsval  17083  mreexd  17268  mreexexlemd  17270  iscat  17298  cidfval  17302  iscatd2  17307  catcocl  17311  catass  17312  catpropd  17335  cidpropd  17336  moni  17365  monpropd  17366  issubc  17466  subccocl  17476  funcco  17502  funcpropd  17532  fullpropd  17552  nati  17587  natpropd  17610  fucpropd  17611  xpcpropd  17842  curfuncf  17872  curf2ndf  17881  yonffthlem  17916  acsfiindd  18186  mndpropd  18325  mhmeql  18379  smndex1mgm  18461  isgrpinv  18547  dfgrp3lem  18588  mhmmnd  18612  cycsubm  18736  cycsubmcom  18738  conjnmzb  18784  gass  18822  symgextf  18940  dfod2  19086  gexdvds  19104  sylow3lem2  19148  efgredlem  19268  efgredeu  19273  ghmcmn  19348  oddvdssubg  19371  dprdfcntz  19533  pgpfaclem3  19601  issrg  19658  isring  19702  dvdsrmul1  19810  issubdrg  19964  islmhm2  20215  lmhmeql  20232  lssacsex  20321  isphl  20745  uvcf1  20909  lindfmm  20944  issubassa2  21006  opsrval  21157  mhpmulcl  21249  scmatmats  21568  smatvscl  21581  mdetunilem7  21675  gsummatr01lem4  21715  m2cpmfo  21813  pmatcollpw3fi1lem1  21843  pm2mpf1lem  21851  pm2mpf1  21856  mp2pm2mplem4  21866  pm2mpghm  21873  chfacfscmulfsupp  21916  chfacfpmmulfsupp  21920  cctop  22064  neiptoptop  22190  neiptopreu  22192  tgrest  22218  ordtrest2lem  22262  cnss1  22335  cncnp  22339  isnrm3  22418  uncmp  22462  cmpfi  22467  iunconn  22487  1stcrest  22512  subislly  22540  islly2  22543  cldllycmp  22554  lly1stc  22555  llycmpkgen2  22609  kgencn  22615  xkoccn  22678  ptcnplem  22680  pthaus  22697  txhaus  22706  txkgen  22711  xkohaus  22712  xkococnlem  22718  txconn  22748  regr1lem2  22799  kqreglem1  22800  reghmph  22852  nrmhmph  22853  trfil2  22946  ufileu  22978  flimopn  23034  flimcf  23041  fclscf  23084  ufilcmp  23091  cnpfcf  23100  cnextfun  23123  tgpmulg  23152  symgtgp  23165  tgpt0  23178  qustgplem  23180  ustex2sym  23276  ustex3sym  23277  trust  23289  restutop  23297  restutopopn  23298  ustuqtop4  23304  utop3cls  23311  utopreg  23312  cstucnd  23344  ucncn  23345  trcfilu  23354  neipcfilu  23356  ismet2  23394  metequiv2  23572  metcnp  23603  metcnp2  23604  metcnpi3  23608  txmetcnp  23609  metustto  23615  metustsym  23617  metust  23620  cfilucfil  23621  metuel2  23627  psmetutop  23629  restmetu  23632  metucn  23633  ngptgp  23698  tngngp  23724  nmoleub  23801  icccmp  23894  reconnlem2  23896  reconn  23897  xmetdcn2  23906  metdseq0  23923  metdscn  23925  elcncf2  23959  cncfmet  23978  cnheibor  24024  nmoleub2lem2  24185  nmoleub3  24188  cvsi  24199  iscfil2  24335  iscfil3  24342  cfilfcls  24343  equivcfil  24368  caubl  24377  bcthlem5  24397  pmltpc  24519  ovollb2  24558  ovoliunnul  24576  ovolicc2lem4  24589  volsup  24625  ioorf  24642  dyadss  24663  dyaddisjlem  24664  mbfposr  24721  cncombf  24727  mbflimsup  24735  i1fmulclem  24772  mbfi1fseqlem4  24788  iblss2  24875  ellimc2  24946  ellimc3  24948  dvnadd  24998  dvmptfsum  25044  dvferm1  25054  dvferm2  25056  fta1g  25237  plyeq0lem  25276  plydivex  25362  fta1  25373  aalioulem2  25398  aalioulem3  25399  ulmuni  25456  ulmbdd  25462  ulmdvlem3  25466  mtest  25468  abelthlem8  25503  efopn  25718  cxpmul2z  25751  cxpcn3lem  25805  jensen  26043  lgambdd  26091  lgamucov  26092  isppw2  26169  mersenne  26280  dchrelbas3  26291  dchrptlem1  26317  dchrpt  26320  lgsval2lem  26360  lgsdchrval  26407  lgsquad3  26440  2sqb  26485  2sqmo  26490  pntrsumbnd2  26620  pntpbnd  26641  pntibnd  26646  istrkgc  26719  istrkgb  26720  tgjustr  26739  tglowdim1i  26766  tgbtwndiff  26771  tgifscgr  26773  iscgrglt  26779  tgcgrxfr  26783  lnext  26832  tgbtwnconn1lem3  26839  tgbtwnconn1  26840  legval  26849  legov  26850  legov2  26851  legtrd  26854  legtri3  26855  legso  26864  hlcgrex  26881  hlcgreu  26883  tglnne  26893  tglndim0  26894  tglineeltr  26896  tglinethru  26901  tglnne0  26905  tglnpt2  26906  colline  26914  tglowdim2l  26915  tglowdim2ln  26916  mirreu3  26919  miriso  26935  midexlem  26957  isperp  26977  perpcom  26978  perpneq  26979  isperp2  26980  footexALT  26983  footex  26986  colperpexlem3  26997  opphllem  27000  midex  27002  oppne3  27008  opptgdim2  27010  opphllem2  27013  opphllem3  27014  opphllem5  27016  opphllem6  27017  opphl  27019  outpasch  27020  lnopp2hpgb  27028  colopp  27034  lmieu  27049  trgcopy  27069  trgcopyeu  27071  iscgra1  27075  cgrane1  27077  cgrane2  27078  cgrane3  27079  cgrahl1  27081  cgrahl2  27082  cgracgr  27083  cgraswap  27085  cgracom  27087  cgratr  27088  flatcgra  27089  cgrabtwn  27091  cgrahl  27092  dfcgra2  27095  sacgr  27096  acopyeu  27099  inaghl  27110  cgrg3col4  27118  f1otrg  27136  f1otrge  27137  axsegcon  27198  axeuclidlem  27233  upgr1eopALT  27390  usgr1eop  27520  pthdepisspth  28004  wpthswwlks2on  28227  clwwlkf1  28314  clwwlknscsh  28327  2pthfrgr  28549  n4cyclfrgr  28556  frgrwopreglem5  28586  frgrwopreglem5ALT  28587  friendshipgt3  28663  smcnlem  28960  0lno  29053  ubthlem1  29133  ubthlem3  29135  chocunii  29564  occl  29567  5oalem1  29917  3oalem2  29926  nmopub2tALT  30172  nmfnleub2  30189  lnconi  30296  kbass5  30383  mdslmd1lem1  30588  mdslmd1lem2  30589  cdj1i  30696  opreu2reuALT  30726  disjabrex  30822  disjabrexf  30823  2ndresdju  30887  acunirnmpt  30898  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1lem  30901  fnpreimac  30910  fgreu  30911  suppovss  30919  xrge0infss  30985  xrofsup  30992  fsumiunle  31045  s3f1  31123  ccatf1  31125  swrdf1  31130  ressprs  31143  dfmgc2  31176  mgcf1o  31183  xrge0addgt0  31202  gsumle  31252  psgnfzto1stlem  31269  fzto1st1  31271  cycpmco2  31302  cycpmrn  31312  cyc3genpm  31321  cycpmconjs  31325  cyc3conja  31326  submarchi  31342  isarchi3  31343  archiabllem1  31349  archiabllem2a  31350  suborng  31416  isarchiofld  31418  imaslmod  31455  nsgqusf1olem2  31501  intlidl  31504  rhmpreimaidl  31505  elrspunidl  31508  rhmimaidl  31511  prmidl2  31518  isprmidlc  31525  rhmpreimaprmidl  31529  qsidomlem2  31531  mxidlprm  31542  ssmxidl  31544  lindsunlem  31607  lindsun  31608  dimkerim  31610  fedgmullem1  31612  fedgmul  31614  mdetpmtr1  31675  txomap  31686  qtophaus  31688  cmpcref  31702  zarclsun  31722  zarclssn  31725  zarcmplem  31733  pstmxmet  31749  sqsscirc1  31760  ordtrest2NEWlem  31774  ordtconnlem1  31776  pnfneige0  31803  lmxrge0  31804  lmdvg  31805  qqhval2  31832  esumcst  31931  esumrnmpt2  31936  esumfsup  31938  esumcvg  31954  esum2d  31961  esumiun  31962  sigaclfu2  31989  insiga  32005  ldsysgenld  32028  ldgenpisyslem1  32031  fiunelros  32042  measinb  32089  imambfm  32129  oms0  32164  omssubadd  32167  carsgclctunlem3  32187  eulerpartlemgvv  32243  dstrvprob  32338  sgnsub  32411  signstfvneq0  32451  actfunsnrndisj  32485  reprinfz1  32502  breprexp  32513  afsval  32551  derangenlem  33033  sconnpi1  33101  cvmsss2  33136  cvmopnlem  33140  cvmlift3lem7  33187  msrval  33400  ttrcltr  33702  naddssim  33764  nosupno  33833  noinfno  33848  noetasuplem4  33866  noetalem1  33871  madebday  34007  cofcutr  34019  ifscgr  34273  cgrxfr  34284  btwnconn1lem13  34328  outsideofeu  34360  neibastop2lem  34476  irrdifflemf  35423  irrdiff  35424  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem14  35718  poimirlem22  35726  poimirlem29  35733  broucube  35738  heicant  35739  mblfinlem1  35741  itg2addnclem  35755  ftc1cnnc  35776  ftc1anclem7  35783  sstotbnd2  35859  equivtotbnd  35863  isbnd3  35869  ssbnd  35873  totbndbnd  35874  cntotbnd  35881  heibor1lem  35894  rrncmslem  35917  lssats  36953  lsat0cv  36974  lkrlss  37036  lfl1dim  37062  lfl1dim2N  37063  lkrpssN  37104  hlhgt2  37330  3dim2  37409  2dim  37411  lplncvrlvol  37557  paddasslem11  37771  pmapjat1  37794  2polssN  37856  pclfinclN  37891  pexmidlem8N  37918  lhpexle1lem  37948  4atex  38017  ltrnid  38076  trlator0  38112  cdlemg2cex  38532  tendodi1  38725  tendodi2  38726  diblss  39111  dihopelvalcpre  39189  dihatexv  39279  mapdval4N  39573  sticksstones8  40037  sticksstones12  40042  sticksstones22  40052  metakunt1  40053  metakunt2  40054  frlmsnic  40188  fsuppind  40202  sn-subeu  40329  sn-0tie0  40342  prjspersym  40367  dffltz  40387  nna4b4nsq  40413  mzpindd  40484  mzpsubst  40486  mzpcompact2lem  40489  eldioph2b  40501  irrapxlem3  40562  irrapxlem5  40564  pellex  40573  pell1234qrdich  40599  pell14qrexpcl  40605  congabseq  40712  jm2.26a  40738  jm2.26lem3  40739  rmydioph  40752  lnrfg  40860  hbt  40871  rfovcnvf1od  41501  clsk3nimkb  41539  ntrneiiso  41590  ntrneikb  41593  ntrneixb  41594  ntrneik3  41595  ntrneix3  41596  ntrneik13  41597  ntrneix13  41598  4an4132  42008  iunconnlem2  42444  fnchoice  42461  cncmpmax  42464  ssinc  42526  ssdec  42527  disjf1  42609  supxrge  42767  suplesup  42768  infxr  42796  infleinf  42801  unb2ltle  42845  rexabslelem  42848  uzub  42861  supminfxr  42894  climrec  43034  climsuse  43039  islptre  43050  addlimc  43079  0ellimcdiv  43080  limsuppnfdlem  43132  limsupub  43135  limsuppnflem  43141  limsupubuz  43144  climinf3  43147  limsupmnflem  43151  climxrre  43181  liminfreuzlem  43233  liminflimsupclim  43238  xlimliminflimsup  43293  icccncfext  43318  cncfiooicclem1  43324  fperdvper  43350  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem2  43378  stoweidlem7  43438  stoweidlem34  43465  stoweidlem52  43483  stoweidlem60  43491  wallispilem3  43498  fourierdlem34  43572  fourierdlem38  43576  fourierdlem39  43577  fourierdlem48  43585  fourierdlem50  43587  fourierdlem51  43588  fourierdlem73  43610  fourierdlem76  43613  fourierdlem77  43614  fourierdlem80  43617  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  etransclem32  43697  etransclem33  43698  sge0f1o  43810  sge0pr  43822  sge0isum  43855  iundjiun  43888  meaiininclem  43914  pimdecfgtioo  44141  pimincfltioo  44142  preimageiingt  44144  preimaleiinlt  44145  smflimlem2  44194  smflimlem4  44196  smfmullem3  44214  smflimmpt  44230  smfinflem  44237  cfsetsnfsetfo  44441  funressnbrafv2  44623  imasetpreimafvbijlemf1  44744  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbnd  45149  isomuspgrlem2  45173  mgmhmeql  45245  isrng  45322  2zlidl  45380  lindslinindsimp2  45692  snlindsntor  45700  lincresunit2  45707  islindeps2  45712