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  6298  fsnex  7229  soisoi  7274  f1o2ndf1  8064  fimaproj  8077  fprlem2  8243  tz7.49  8376  omabs  8579  cofon1  8600  naddssim  8613  omxpenlem  9006  fopwdom  9013  findcard3  9183  frfi  9185  finsschain  9259  marypha1lem  9336  wemappo  9454  wdomtr  9480  cantnfp1  9590  ttrcltr  9625  harcard  9890  numacn  9959  infunsdom1  10122  sornom  10187  ssfin4  10220  fin1a2lem11  10320  fin1a2lem13  10322  fpwwe2lem12  10553  pwfseq  10575  mulcmpblnr  10982  00id  11308  addrid  11313  cnegex  11314  negeu  11370  add20  11649  ltmul12a  11997  lediv12a  12035  cru  12137  qextltlem  13117  xleadd1a  13168  xmullem  13179  xlemul1a  13203  ixxss12  13281  ioodisj  13398  fvf1tp  13709  fsuppmapnn0fz  13919  seqf1o  13966  mulexpz  14025  leexp1a  14098  faclbnd  14213  swrdswrdlem  14627  abs3lem  15262  rexico  15277  cau3lem  15278  rlim3  15421  ello12  15439  lo1bdd2  15447  elo12  15450  rlimconst  15467  isercoll  15591  climcau  15594  climbdd  15595  summolem2  15639  fsumconst  15713  o1fsum  15736  incexclem  15759  fprodconst  15901  bitsfzo  16362  dvdsmulgcd  16483  pc2dvds  16807  pcz  16809  pcadd  16817  pcfac  16827  vdwmc2  16907  vdwlem2  16910  vdwlem10  16918  vdw  16922  ramcl  16957  sbcie3s  17089  firest  17352  prdsval  17375  mreexd  17565  mreexexlemd  17567  iscat  17595  cidfval  17599  iscatd2  17604  catcocl  17608  catass  17609  catpropd  17632  cidpropd  17633  moni  17660  monpropd  17661  issubc  17759  subccocl  17769  funcco  17795  funcpropd  17826  fullpropd  17846  nati  17882  natpropd  17903  fucpropd  17904  xpcpropd  18131  curfuncf  18161  curf2ndf  18170  yonffthlem  18205  acsfiindd  18476  chnind  18544  chnso  18547  mgmhmeql  18641  sgrppropd  18656  mndpropd  18684  mhmeql  18751  smndex1mgm  18832  isgrpinv  18923  dfgrp3lem  18968  mhmmnd  18994  cycsubm  19131  cycsubmcom  19133  conjnmzb  19182  ghmqusnsg  19211  ghmquskerlem3  19215  ghmqusker  19216  gass  19230  symgextf  19346  dfod2  19493  gexdvds  19513  sylow3lem2  19557  efgredlem  19676  efgredeu  19681  ghmcmn  19760  oddvdssubg  19784  dprdfcntz  19946  pgpfaclem3  20014  gsumle  20074  isrng  20089  issrg  20123  isring  20172  dvdsrmul1  20305  issubdrg  20713  suborng  20809  islmhm2  20990  lmhmeql  21007  lssacsex  21099  rhmpreimaidl  21232  rhmqusnsg  21240  isphl  21583  uvcf1  21747  lindfmm  21782  sraassab  21823  issubassa2  21848  opsrval  22001  psdmul  22109  scmatmats  22455  smatvscl  22468  mdetunilem7  22562  gsummatr01lem4  22602  m2cpmfo  22700  pmatcollpw3fi1lem1  22730  pm2mpf1lem  22738  pm2mpf1  22743  mp2pm2mplem4  22753  pm2mpghm  22760  chfacfscmulfsupp  22803  chfacfpmmulfsupp  22807  cctop  22950  neiptoptop  23075  neiptopreu  23077  tgrest  23103  ordtrest2lem  23147  cnss1  23220  cncnp  23224  isnrm3  23303  uncmp  23347  cmpfi  23352  iunconn  23372  1stcrest  23397  subislly  23425  islly2  23428  cldllycmp  23439  lly1stc  23440  llycmpkgen2  23494  kgencn  23500  xkoccn  23563  ptcnplem  23565  pthaus  23582  txhaus  23591  txkgen  23596  xkohaus  23597  xkococnlem  23603  txconn  23633  regr1lem2  23684  kqreglem1  23685  reghmph  23737  nrmhmph  23738  trfil2  23831  ufileu  23863  flimopn  23919  flimcf  23926  fclscf  23969  ufilcmp  23976  cnpfcf  23985  cnextfun  24008  tgpmulg  24037  symgtgp  24050  tgpt0  24063  qustgplem  24065  ustex2sym  24161  ustex3sym  24162  trust  24173  restutop  24181  restutopopn  24182  ustuqtop4  24188  utop3cls  24195  utopreg  24196  cstucnd  24227  ucncn  24228  trcfilu  24237  neipcfilu  24239  ismet2  24277  metequiv2  24454  metcnp  24485  metcnp2  24486  metcnpi3  24490  txmetcnp  24491  metustto  24497  metustsym  24499  metust  24502  cfilucfil  24503  metuel2  24509  psmetutop  24511  restmetu  24514  metucn  24515  ngptgp  24580  tngngp  24598  nmoleub  24675  icccmp  24770  reconnlem2  24772  reconn  24773  xmetdcn2  24782  metdseq0  24799  metdscn  24801  elcncf2  24839  cncfmet  24858  cnheibor  24910  nmoleub2lem2  25072  nmoleub3  25075  cvsi  25086  iscfil2  25222  iscfil3  25229  cfilfcls  25230  equivcfil  25255  caubl  25264  bcthlem5  25284  pmltpc  25407  ovollb2  25446  ovoliunnul  25464  ovolicc2lem4  25477  volsup  25513  ioorf  25530  dyadss  25551  dyaddisjlem  25552  mbfposr  25609  cncombf  25615  mbflimsup  25623  i1fmulclem  25659  mbfi1fseqlem4  25675  iblss2  25763  ellimc2  25834  ellimc3  25836  dvnadd  25887  dvmptfsum  25935  dvferm1  25945  dvferm2  25947  fta1g  26131  plyeq0lem  26171  plydivex  26261  fta1  26272  aalioulem2  26297  aalioulem3  26298  ulmuni  26357  ulmbdd  26363  ulmdvlem3  26367  mtest  26369  abelthlem8  26405  efopn  26623  cxpmul2z  26656  cxpcn3lem  26713  jensen  26955  lgambdd  27003  lgamucov  27004  isppw2  27081  mersenne  27194  dchrelbas3  27205  dchrptlem1  27231  dchrpt  27234  lgsval2lem  27274  lgsdchrval  27321  lgsquad3  27354  2sqb  27399  2sqmo  27404  pntrsumbnd2  27534  pntpbnd  27555  pntibnd  27560  nosupno  27671  noinfno  27686  noetasuplem4  27704  noetalem1  27709  madebday  27896  cofcutr  27920  negsprop  28031  mulscom  28135  absmuls  28240  addonbday  28275  bdayfinbndlem1  28463  z12sge0  28479  remulscl  28498  tgjustr  28546  tglowdim1i  28573  tgbtwndiff  28578  tgifscgr  28580  iscgrglt  28586  tgcgrxfr  28590  lnext  28639  tgbtwnconn1lem3  28646  tgbtwnconn1  28647  legval  28656  legov  28657  legov2  28658  legtrd  28661  legtri3  28662  legso  28671  hlcgrex  28688  hlcgreu  28690  tglnne  28700  tglndim0  28701  tglineeltr  28703  tglinethru  28708  tglnne0  28712  tglnpt2  28713  colline  28721  tglowdim2l  28722  tglowdim2ln  28723  mirreu3  28726  miriso  28742  midexlem  28764  isperp  28784  perpcom  28785  perpneq  28786  isperp2  28787  footexALT  28790  footex  28793  colperpexlem3  28804  opphllem  28807  midex  28809  oppne3  28815  opptgdim2  28817  opphllem2  28820  opphllem3  28821  opphllem5  28823  opphllem6  28824  opphl  28826  outpasch  28827  lnopp2hpgb  28835  colopp  28841  lmieu  28856  trgcopy  28876  trgcopyeu  28878  iscgra1  28882  cgrane1  28884  cgrane2  28885  cgrane3  28886  cgrahl1  28888  cgrahl2  28889  cgracgr  28890  cgraswap  28892  cgracom  28894  cgratr  28895  flatcgra  28896  cgrabtwn  28898  cgrahl  28899  dfcgra2  28902  sacgr  28903  acopyeu  28906  inaghl  28917  cgrg3col4  28925  f1otrg  28943  f1otrge  28944  axsegcon  29000  axeuclidlem  29035  upgr1eopALT  29190  usgr1eop  29323  pthdepisspth  29808  wpthswwlks2on  30037  clwwlkf1  30124  clwwlknscsh  30137  2pthfrgr  30359  n4cyclfrgr  30366  frgrwopreglem5  30396  frgrwopreglem5ALT  30397  friendshipgt3  30473  smcnlem  30772  0lno  30865  ubthlem1  30945  ubthlem3  30947  chocunii  31376  occl  31379  5oalem1  31729  3oalem2  31738  nmopub2tALT  31984  nmfnleub2  32001  lnconi  32108  kbass5  32195  mdslmd1lem1  32400  mdslmd1lem2  32401  cdj1i  32508  opreu2reuALT  32551  disjabrex  32657  disjabrexf  32658  2ndresdju  32727  acunirnmpt  32737  acunirnmpt2  32738  acunirnmpt2f  32739  aciunf1lem  32740  fnpreimac  32749  fgreu  32750  suppovss  32760  xrge0infss  32840  xrofsup  32847  elq2  32892  fsumiunle  32910  sgnsub  32918  2exple2exp  32926  s3f1  33029  ccatf1  33031  ccatws1f1o  33033  swrdf1  33038  ressprs  33048  dfmgc2  33078  mgcf1o  33085  xrge0addgt0  33099  mndlrinvb  33107  mndlactf1  33108  mndlactfo  33109  mndractf1  33110  mndractfo  33111  mndlactf1o  33112  gsumfs2d  33144  gsumwun  33158  gsumwrd2dccatlem  33159  psgnfzto1stlem  33182  fzto1st1  33184  cycpmco2  33215  cycpmrn  33225  cyc3genpm  33234  cycpmconjs  33238  cyc3conja  33239  conjga  33252  fxpsubrg  33256  submarchi  33268  isarchi3  33269  archiabllem1  33275  archiabllem2a  33276  isarchiofld  33281  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem2  33330  erler  33347  rlocaddval  33350  rlocmulval  33351  rloccring  33352  rloc1r  33354  subrdom  33367  isdrng4  33377  fracfld  33390  imaslmod  33434  dvdsruasso  33466  unitprodclb  33470  nsgqusf1olem2  33495  lmhmqusker  33498  intlidl  33501  rhmquskerlem  33506  elrspunidl  33509  elrspunsn  33510  rhmimaidl  33513  prmidl2  33522  isprmidlc  33528  rhmpreimaprmidl  33532  qsidomlem2  33534  ssdifidllem  33537  ssdifidlprm  33539  mxidlprm  33551  ssmxidl  33555  opprqusplusg  33570  opprqusmulr  33572  qsdrngilem  33575  qsdrngi  33576  rsprprmprmidl  33603  rsprprmprmidlb  33604  rprmirred  33612  rprmirredb  33613  rprmdvdspow  33614  rprmdvdsprod  33615  1arithidom  33618  1arithufdlem2  33626  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  dfufd2  33631  zringfrac  33635  deg1prod  33664  ply1dg3rt0irred  33665  r1plmhm  33691  r1pquslmic  33692  extvfvcl  33701  mplmulmvr  33704  mplvrpmga  33710  esplyfval3  33730  esplyind  33731  exsslsb  33753  lindsunlem  33781  lindsun  33782  dimkerim  33784  fedgmullem1  33786  fedgmul  33788  dimlssid  33789  evls1fldgencl  33827  fldextrspunlsplem  33830  extdgfialg  33851  minplyirred  33868  fldext2chn  33885  constrmon  33901  constrconj  33902  constrfin  33903  constrelextdg2  33904  constrextdg2lem  33905  constrextdg2  33906  constrext2chnlem  33907  constrfiss  33908  cos9thpiminplylem2  33940  mdetpmtr1  33980  txomap  33991  qtophaus  33993  cmpcref  34007  zarclsun  34027  zarclssn  34030  zarcmplem  34038  pstmxmet  34054  sqsscirc1  34065  ordtrest2NEWlem  34079  ordtconnlem1  34081  pnfneige0  34108  lmxrge0  34109  lmdvg  34110  qqhval2  34139  esumcst  34220  esumrnmpt2  34225  esumfsup  34227  esumcvg  34243  esum2d  34250  esumiun  34251  sigaclfu2  34278  insiga  34294  ldsysgenld  34317  ldgenpisyslem1  34320  fiunelros  34331  measinb  34378  imambfm  34419  oms0  34454  omssubadd  34457  carsgclctunlem3  34477  eulerpartlemgvv  34533  dstrvprob  34629  signstfvneq0  34729  actfunsnrndisj  34762  reprinfz1  34779  breprexp  34790  afsval  34828  derangenlem  35365  sconnpi1  35433  cvmsss2  35468  cvmopnlem  35472  cvmlift3lem7  35519  msrval  35732  ifscgr  36238  cgrxfr  36249  btwnconn1lem13  36293  outsideofeu  36325  neibastop2lem  36554  weiunso  36660  irrdifflemf  37526  irrdiff  37527  matunitlindflem1  37813  matunitlindflem2  37814  poimirlem14  37831  poimirlem22  37839  poimirlem29  37846  broucube  37851  heicant  37852  mblfinlem1  37854  itg2addnclem  37868  ftc1cnnc  37889  ftc1anclem7  37896  sstotbnd2  37971  equivtotbnd  37975  isbnd3  37981  ssbnd  37985  totbndbnd  37986  cntotbnd  37993  heibor1lem  38006  rrncmslem  38029  lssats  39268  lsat0cv  39289  lkrlss  39351  lfl1dim  39377  lfl1dim2N  39378  lkrpssN  39419  hlhgt2  39645  3dim2  39724  2dim  39726  lplncvrlvol  39872  paddasslem11  40086  pmapjat1  40109  2polssN  40171  pclfinclN  40206  pexmidlem8N  40233  lhpexle1lem  40263  4atex  40332  ltrnid  40391  trlator0  40427  cdlemg2cex  40847  tendodi1  41040  tendodi2  41041  diblss  41426  dihopelvalcpre  41504  dihatexv  41594  mapdval4N  41888  fldhmf1  42340  mndmolinv  42345  primrootscoprmpow  42349  posbezout  42350  primrootscoprbij2  42353  primrootspoweq0  42356  aks6d1c2p2  42369  hashscontpow  42372  aks6d1c2lem4  42377  aks6d1c2  42380  aks6d1c5  42389  sticksstones8  42403  sticksstones12  42408  sticksstones22  42418  aks6d1c6lem3  42422  aks6d1c6isolem1  42424  unitscyglem3  42447  aks5  42454  sn-subeu  42678  sn-0tie0  42702  fiabv  42787  frlmsnic  42791  fsuppind  42829  prjspersym  42846  dffltz  42873  nna4b4nsq  42899  mzpindd  42984  mzpsubst  42986  mzpcompact2lem  42989  eldioph2b  43001  irrapxlem3  43062  irrapxlem5  43064  pellex  43073  pell1234qrdich  43099  pell14qrexpcl  43105  congabseq  43212  jm2.26a  43238  jm2.26lem3  43239  rmydioph  43252  lnrfg  43357  hbt  43368  cantnftermord  43558  cantnfresb  43562  cantnf2  43563  oawordex2  43564  omabs2  43570  tfsconcatfv  43579  tfsconcatrev  43586  ofoaass  43598  nadd2rabtr  43622  nadd1suc  43630  naddgeoa  43632  rfovcnvf1od  44241  clsk3nimkb  44277  ntrneiiso  44328  ntrneikb  44331  ntrneixb  44332  ntrneik3  44333  ntrneix3  44334  ntrneik13  44335  ntrneix13  44336  4an4132  44736  iunconnlem2  45171  modelaxrep  45218  fnchoice  45270  cncmpmax  45273  ssinc  45327  ssdec  45328  disjf1  45423  supxrge  45579  suplesup  45580  infxr  45607  infleinf  45612  unb2ltle  45655  rexabslelem  45658  uzub  45671  supminfxr  45704  climrec  45845  climsuse  45850  islptre  45861  addlimc  45888  0ellimcdiv  45889  limsuppnfdlem  45941  limsupub  45944  limsuppnflem  45950  limsupubuz  45953  climinf3  45956  limsupmnflem  45960  climxrre  45990  liminfreuzlem  46042  liminflimsupclim  46047  xlimliminflimsup  46102  icccncfext  46127  cncfiooicclem1  46133  fperdvper  46159  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvmptfprodlem  46184  dvmptfprod  46185  dvnprodlem2  46187  stoweidlem7  46247  stoweidlem34  46274  stoweidlem52  46292  stoweidlem60  46300  wallispilem3  46307  fourierdlem34  46381  fourierdlem38  46385  fourierdlem39  46386  fourierdlem48  46394  fourierdlem50  46396  fourierdlem51  46397  fourierdlem73  46419  fourierdlem76  46422  fourierdlem77  46423  fourierdlem80  46426  fourierdlem87  46433  fourierdlem103  46449  fourierdlem104  46450  etransclem32  46506  etransclem33  46507  sge0f1o  46622  sge0pr  46634  sge0isum  46667  iundjiun  46700  meaiininclem  46726  pimdecfgtioo  46957  pimincfltioo  46958  preimageiingt  46960  preimaleiinlt  46961  smflimlem2  47012  smflimlem4  47014  smfmullem3  47033  smflimmpt  47050  smfinflem  47057  smfpimne2  47080  fsupdm  47082  finfdm  47086  cfsetsnfsetfo  47302  funressnbrafv2  47486  imasetpreimafvbijlemf1  47646  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  bgoldbtbnd  48051  isuspgrim  48138  stgrusgra  48201  isubgr3stgrlem6  48213  2zlidl  48482  lindslinindsimp2  48705  snlindsntor  48713  lincresunit2  48720  islindeps2  48725  imaf1co  49396  imasubc3  49397  fucofvalg  49559  fuco21  49577  precofvalALT  49609  lanfval  49854  ranfval  49855