Theorem simpllr 776

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 732	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  6304  fsnex  7238  soisoi  7283  f1o2ndf1  8072  fimaproj  8085  fprlem2  8251  tz7.49  8384  omabs  8587  cofon1  8608  naddssim  8621  omxpenlem  9016  fopwdom  9023  findcard3  9193  frfi  9195  finsschain  9269  marypha1lem  9346  wemappo  9464  wdomtr  9490  cantnfp1  9602  ttrcltr  9637  harcard  9902  numacn  9971  infunsdom1  10134  sornom  10199  ssfin4  10232  fin1a2lem11  10332  fin1a2lem13  10334  fpwwe2lem12  10565  pwfseq  10587  mulcmpblnr  10994  00id  11321  addrid  11326  cnegex  11327  negeu  11383  add20  11662  ltmul12a  12011  lediv12a  12049  cru  12151  qextltlem  13154  xleadd1a  13205  xmullem  13216  xlemul1a  13240  ixxss12  13318  ioodisj  13435  fvf1tp  13748  fsuppmapnn0fz  13958  seqf1o  14005  mulexpz  14064  leexp1a  14137  faclbnd  14252  swrdswrdlem  14666  abs3lem  15301  rexico  15316  cau3lem  15317  rlim3  15460  ello12  15478  lo1bdd2  15486  elo12  15489  rlimconst  15506  isercoll  15630  climcau  15633  climbdd  15634  summolem2  15678  fsumconst  15752  o1fsum  15776  incexclem  15801  fprodconst  15943  bitsfzo  16404  dvdsmulgcd  16525  pc2dvds  16850  pcz  16852  pcadd  16860  pcfac  16870  vdwmc2  16950  vdwlem2  16953  vdwlem10  16961  vdw  16965  ramcl  17000  sbcie3s  17132  firest  17395  prdsval  17418  mreexd  17608  mreexexlemd  17610  iscat  17638  cidfval  17642  iscatd2  17647  catcocl  17651  catass  17652  catpropd  17675  cidpropd  17676  moni  17703  monpropd  17704  issubc  17802  subccocl  17812  funcco  17838  funcpropd  17869  fullpropd  17889  nati  17925  natpropd  17946  fucpropd  17947  xpcpropd  18174  curfuncf  18204  curf2ndf  18213  yonffthlem  18248  acsfiindd  18519  chnind  18587  chnso  18590  mgmhmeql  18684  sgrppropd  18699  mndpropd  18727  mhmeql  18794  smndex1mgm  18878  isgrpinv  18969  dfgrp3lem  19014  mhmmnd  19040  cycsubm  19177  cycsubmcom  19179  conjnmzb  19228  ghmqusnsg  19257  ghmquskerlem3  19261  ghmqusker  19262  gass  19276  symgextf  19392  dfod2  19539  gexdvds  19559  sylow3lem2  19603  efgredlem  19722  efgredeu  19727  ghmcmn  19806  oddvdssubg  19830  dprdfcntz  19992  pgpfaclem3  20060  gsumle  20120  isrng  20135  issrg  20169  isring  20218  dvdsrmul1  20349  issubdrg  20757  suborng  20853  islmhm2  21033  lmhmeql  21050  lssacsex  21142  rhmpreimaidl  21275  rhmqusnsg  21283  isphl  21608  uvcf1  21772  lindfmm  21807  sraassab  21848  issubassa2  21872  opsrval  22024  psdmul  22132  scmatmats  22476  smatvscl  22489  mdetunilem7  22583  gsummatr01lem4  22623  m2cpmfo  22721  pmatcollpw3fi1lem1  22751  pm2mpf1lem  22759  pm2mpf1  22764  mp2pm2mplem4  22774  pm2mpghm  22781  chfacfscmulfsupp  22824  chfacfpmmulfsupp  22828  cctop  22971  neiptoptop  23096  neiptopreu  23098  tgrest  23124  ordtrest2lem  23168  cnss1  23241  cncnp  23245  isnrm3  23324  uncmp  23368  cmpfi  23373  iunconn  23393  1stcrest  23418  subislly  23446  islly2  23449  cldllycmp  23460  lly1stc  23461  llycmpkgen2  23515  kgencn  23521  xkoccn  23584  ptcnplem  23586  pthaus  23603  txhaus  23612  txkgen  23617  xkohaus  23618  xkococnlem  23624  txconn  23654  regr1lem2  23705  kqreglem1  23706  reghmph  23758  nrmhmph  23759  trfil2  23852  ufileu  23884  flimopn  23940  flimcf  23947  fclscf  23990  ufilcmp  23997  cnpfcf  24006  cnextfun  24029  tgpmulg  24058  symgtgp  24071  tgpt0  24084  qustgplem  24086  ustex2sym  24182  ustex3sym  24183  trust  24194  restutop  24202  restutopopn  24203  ustuqtop4  24209  utop3cls  24216  utopreg  24217  cstucnd  24248  ucncn  24249  trcfilu  24258  neipcfilu  24260  ismet2  24298  metequiv2  24475  metcnp  24506  metcnp2  24507  metcnpi3  24511  txmetcnp  24512  metustto  24518  metustsym  24520  metust  24523  cfilucfil  24524  metuel2  24530  psmetutop  24532  restmetu  24535  metucn  24536  ngptgp  24601  tngngp  24619  nmoleub  24696  icccmp  24791  reconnlem2  24793  reconn  24794  xmetdcn2  24803  metdseq0  24820  metdscn  24822  elcncf2  24857  cncfmet  24876  cnheibor  24922  nmoleub2lem2  25083  nmoleub3  25086  cvsi  25097  iscfil2  25233  iscfil3  25240  cfilfcls  25241  equivcfil  25266  caubl  25275  bcthlem5  25295  pmltpc  25417  ovollb2  25456  ovoliunnul  25474  ovolicc2lem4  25487  volsup  25523  ioorf  25540  dyadss  25561  dyaddisjlem  25562  mbfposr  25619  cncombf  25625  mbflimsup  25633  i1fmulclem  25669  mbfi1fseqlem4  25685  iblss2  25773  ellimc2  25844  ellimc3  25846  dvnadd  25896  dvmptfsum  25942  dvferm1  25952  dvferm2  25954  fta1g  26135  plyeq0lem  26175  plydivex  26263  fta1  26274  aalioulem2  26299  aalioulem3  26300  ulmuni  26357  ulmbdd  26363  ulmdvlem3  26367  mtest  26369  abelthlem8  26404  efopn  26622  cxpmul2z  26655  cxpcn3lem  26711  jensen  26952  lgambdd  27000  lgamucov  27001  isppw2  27078  mersenne  27190  dchrelbas3  27201  dchrptlem1  27227  dchrpt  27230  lgsval2lem  27270  lgsdchrval  27317  lgsquad3  27350  2sqb  27395  2sqmo  27400  pntrsumbnd2  27530  pntpbnd  27551  pntibnd  27556  nosupno  27667  noinfno  27682  noetasuplem4  27700  noetalem1  27705  madebday  27892  cofcutr  27916  negsprop  28027  mulscom  28131  absmuls  28236  addonbday  28271  bdayfinbndlem1  28459  z12sge0  28475  remulscl  28494  tgjustr  28542  tglowdim1i  28569  tgbtwndiff  28574  tgifscgr  28576  iscgrglt  28582  tgcgrxfr  28586  lnext  28635  tgbtwnconn1lem3  28642  tgbtwnconn1  28643  legval  28652  legov  28653  legov2  28654  legtrd  28657  legtri3  28658  legso  28667  hlcgrex  28684  hlcgreu  28686  tglnne  28696  tglndim0  28697  tglineeltr  28699  tglinethru  28704  tglnne0  28708  tglnpt2  28709  colline  28717  tglowdim2l  28718  tglowdim2ln  28719  mirreu3  28722  miriso  28738  midexlem  28760  isperp  28780  perpcom  28781  perpneq  28782  isperp2  28783  footexALT  28786  footex  28789  colperpexlem3  28800  opphllem  28803  midex  28805  oppne3  28811  opptgdim2  28813  opphllem2  28816  opphllem3  28817  opphllem5  28819  opphllem6  28820  opphl  28822  outpasch  28823  lnopp2hpgb  28831  colopp  28837  lmieu  28852  trgcopy  28872  trgcopyeu  28874  iscgra1  28878  cgrane1  28880  cgrane2  28881  cgrane3  28882  cgrahl1  28884  cgrahl2  28885  cgracgr  28886  cgraswap  28888  cgracom  28890  cgratr  28891  flatcgra  28892  cgrabtwn  28894  cgrahl  28895  dfcgra2  28898  sacgr  28899  acopyeu  28902  inaghl  28913  cgrg3col4  28921  f1otrg  28939  f1otrge  28940  axsegcon  28996  axeuclidlem  29031  upgr1eopALT  29186  usgr1eop  29319  pthdepisspth  29803  wpthswwlks2on  30032  clwwlkf1  30119  clwwlknscsh  30132  2pthfrgr  30354  n4cyclfrgr  30361  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  friendshipgt3  30468  smcnlem  30768  0lno  30861  ubthlem1  30941  ubthlem3  30943  chocunii  31372  occl  31375  5oalem1  31725  3oalem2  31734  nmopub2tALT  31980  nmfnleub2  31997  lnconi  32104  kbass5  32191  mdslmd1lem1  32396  mdslmd1lem2  32397  cdj1i  32504  opreu2reuALT  32546  disjabrex  32652  disjabrexf  32653  2ndresdju  32722  acunirnmpt  32732  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1lem  32735  fnpreimac  32743  fgreu  32744  suppovss  32754  xrge0infss  32833  xrofsup  32840  elq2  32885  fsumiunle  32902  sgnsub  32910  2exple2exp  32918  s3f1  33007  ccatf1  33009  ccatws1f1o  33011  swrdf1  33016  ressprs  33026  dfmgc2  33056  mgcf1o  33063  xrge0addgt0  33077  mndlrinvb  33085  mndlactf1  33086  mndlactfo  33087  mndractf1  33088  mndractfo  33089  mndlactf1o  33090  gsumfs2d  33122  suppgsumssiun  33133  gsumwun  33137  gsumwrd2dccatlem  33138  psgnfzto1stlem  33161  fzto1st1  33163  cycpmco2  33194  cycpmrn  33204  cyc3genpm  33213  cycpmconjs  33217  cyc3conja  33218  conjga  33231  fxpsubrg  33235  submarchi  33247  isarchi3  33248  archiabllem1  33254  archiabllem2a  33255  isarchiofld  33260  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem2  33309  erler  33326  rlocaddval  33329  rlocmulval  33330  rloccring  33331  rloc1r  33333  subrdom  33346  isdrng4  33356  fracfld  33369  imaslmod  33413  dvdsruasso  33445  unitprodclb  33449  nsgqusf1olem2  33474  lmhmqusker  33477  intlidl  33480  rhmquskerlem  33485  elrspunidl  33488  elrspunsn  33489  rhmimaidl  33492  prmidl2  33501  isprmidlc  33507  rhmpreimaprmidl  33511  qsidomlem2  33513  ssdifidllem  33516  ssdifidlprm  33518  mxidlprm  33530  ssmxidl  33534  opprqusplusg  33549  opprqusmulr  33551  qsdrngilem  33554  qsdrngi  33555  rsprprmprmidl  33582  rsprprmprmidlb  33583  rprmirred  33591  rprmirredb  33592  rprmdvdspow  33593  rprmdvdsprod  33594  1arithidom  33597  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  dfufd2  33610  zringfrac  33614  deg1prod  33643  ply1dg3rt0irred  33644  r1plmhm  33670  r1pquslmic  33671  extvfvcl  33680  mplmulmvr  33683  mplvrpmga  33689  psrgsum  33692  psrmonprod  33696  esplyfval3  33716  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  exsslsb  33741  lindsunlem  33768  lindsun  33769  dimkerim  33771  fedgmullem1  33773  fedgmul  33775  dimlssid  33776  evls1fldgencl  33814  fldextrspunlsplem  33817  extdgfialg  33838  minplyirred  33855  fldext2chn  33872  constrmon  33888  constrconj  33889  constrfin  33890  constrelextdg2  33891  constrextdg2lem  33892  constrextdg2  33893  constrext2chnlem  33894  constrfiss  33895  cos9thpiminplylem2  33927  mdetpmtr1  33967  txomap  33978  qtophaus  33980  cmpcref  33994  zarclsun  34014  zarclssn  34017  zarcmplem  34025  pstmxmet  34041  sqsscirc1  34052  ordtrest2NEWlem  34066  ordtconnlem1  34068  pnfneige0  34095  lmxrge0  34096  lmdvg  34097  qqhval2  34126  esumcst  34207  esumrnmpt2  34212  esumfsup  34214  esumcvg  34230  esum2d  34237  esumiun  34238  sigaclfu2  34265  insiga  34281  ldsysgenld  34304  ldgenpisyslem1  34307  fiunelros  34318  measinb  34365  imambfm  34406  oms0  34441  omssubadd  34444  carsgclctunlem3  34464  eulerpartlemgvv  34520  dstrvprob  34616  signstfvneq0  34716  actfunsnrndisj  34749  reprinfz1  34766  breprexp  34777  afsval  34815  derangenlem  35353  sconnpi1  35421  cvmsss2  35456  cvmopnlem  35460  cvmlift3lem7  35507  msrval  35720  ifscgr  36226  cgrxfr  36237  btwnconn1lem13  36281  outsideofeu  36313  neibastop2lem  36542  weiunso  36648  irrdifflemf  37639  irrdiff  37640  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem14  37955  poimirlem22  37963  poimirlem29  37970  broucube  37975  heicant  37976  mblfinlem1  37978  itg2addnclem  37992  ftc1cnnc  38013  ftc1anclem7  38020  sstotbnd2  38095  equivtotbnd  38099  isbnd3  38105  ssbnd  38109  totbndbnd  38110  cntotbnd  38117  heibor1lem  38130  rrncmslem  38153  lssats  39458  lsat0cv  39479  lkrlss  39541  lfl1dim  39567  lfl1dim2N  39568  lkrpssN  39609  hlhgt2  39835  3dim2  39914  2dim  39916  lplncvrlvol  40062  paddasslem11  40276  pmapjat1  40299  2polssN  40361  pclfinclN  40396  pexmidlem8N  40423  lhpexle1lem  40453  4atex  40522  ltrnid  40581  trlator0  40617  cdlemg2cex  41037  tendodi1  41230  tendodi2  41231  diblss  41616  dihopelvalcpre  41694  dihatexv  41784  mapdval4N  42078  fldhmf1  42529  mndmolinv  42534  primrootscoprmpow  42538  posbezout  42539  primrootscoprbij2  42542  primrootspoweq0  42545  aks6d1c2p2  42558  hashscontpow  42561  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5  42578  sticksstones8  42592  sticksstones12  42597  sticksstones22  42607  aks6d1c6lem3  42611  aks6d1c6isolem1  42613  unitscyglem3  42636  aks5  42643  sn-subeu  42859  sn-0tie0  42896  fiabv  42981  frlmsnic  42985  fsuppind  43023  prjspersym  43040  dffltz  43067  nna4b4nsq  43093  mzpindd  43178  mzpsubst  43180  mzpcompact2lem  43183  eldioph2b  43195  irrapxlem3  43252  irrapxlem5  43254  pellex  43263  pell1234qrdich  43289  pell14qrexpcl  43295  congabseq  43402  jm2.26a  43428  jm2.26lem3  43429  rmydioph  43442  lnrfg  43547  hbt  43558  cantnftermord  43748  cantnfresb  43752  cantnf2  43753  oawordex2  43754  omabs2  43760  tfsconcatfv  43769  tfsconcatrev  43776  ofoaass  43788  nadd2rabtr  43812  nadd1suc  43820  naddgeoa  43822  rfovcnvf1od  44431  clsk3nimkb  44467  ntrneiiso  44518  ntrneikb  44521  ntrneixb  44522  ntrneik3  44523  ntrneix3  44524  ntrneik13  44525  ntrneix13  44526  4an4132  44926  iunconnlem2  45361  modelaxrep  45408  fnchoice  45460  cncmpmax  45463  ssinc  45517  ssdec  45518  disjf1  45613  supxrge  45768  suplesup  45769  infxr  45796  infleinf  45801  unb2ltle  45843  rexabslelem  45846  uzub  45859  supminfxr  45892  climrec  46033  climsuse  46038  islptre  46049  addlimc  46076  0ellimcdiv  46077  limsuppnfdlem  46129  limsupub  46132  limsuppnflem  46138  limsupubuz  46141  climinf3  46144  limsupmnflem  46148  climxrre  46178  liminfreuzlem  46230  liminflimsupclim  46235  xlimliminflimsup  46290  icccncfext  46315  cncfiooicclem1  46321  fperdvper  46347  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvmptfprodlem  46372  dvmptfprod  46373  dvnprodlem2  46375  stoweidlem7  46435  stoweidlem34  46462  stoweidlem52  46480  stoweidlem60  46488  wallispilem3  46495  fourierdlem34  46569  fourierdlem38  46573  fourierdlem39  46574  fourierdlem48  46582  fourierdlem50  46584  fourierdlem51  46585  fourierdlem73  46607  fourierdlem76  46610  fourierdlem77  46611  fourierdlem80  46614  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  etransclem32  46694  etransclem33  46695  sge0f1o  46810  sge0pr  46822  sge0isum  46855  iundjiun  46888  meaiininclem  46914  hoicvr  46976  pimdecfgtioo  47145  pimincfltioo  47146  preimageiingt  47148  preimaleiinlt  47149  smflimlem2  47200  smflimlem4  47202  smfmullem3  47221  smflimmpt  47238  smfinflem  47245  smfpimne2  47268  fsupdm  47270  finfdm  47274  cfsetsnfsetfo  47508  funressnbrafv2  47692  imasetpreimafvbijlemf1  47864  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  isuspgrim  48372  stgrusgra  48435  isubgr3stgrlem6  48447  2zlidl  48716  lindslinindsimp2  48939  snlindsntor  48947  lincresunit2  48954  islindeps2  48959  imaf1co  49630  imasubc3  49631  fucofvalg  49793  fuco21  49811  precofvalALT  49843  lanfval  50088  ranfval  50089