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  6298  fsnex  7231  soisoi  7276  f1o2ndf1  8065  fimaproj  8078  fprlem2  8244  tz7.49  8377  omabs  8580  cofon1  8601  naddssim  8614  omxpenlem  9009  fopwdom  9016  findcard3  9186  frfi  9188  finsschain  9262  marypha1lem  9339  wemappo  9457  wdomtr  9483  cantnfp1  9593  ttrcltr  9628  harcard  9893  numacn  9962  infunsdom1  10125  sornom  10190  ssfin4  10223  fin1a2lem11  10323  fin1a2lem13  10325  fpwwe2lem12  10556  pwfseq  10578  mulcmpblnr  10985  00id  11312  addrid  11317  cnegex  11318  negeu  11374  add20  11653  ltmul12a  12002  lediv12a  12040  cru  12142  qextltlem  13145  xleadd1a  13196  xmullem  13207  xlemul1a  13231  ixxss12  13309  ioodisj  13426  fvf1tp  13739  fsuppmapnn0fz  13949  seqf1o  13996  mulexpz  14055  leexp1a  14128  faclbnd  14243  swrdswrdlem  14657  abs3lem  15292  rexico  15307  cau3lem  15308  rlim3  15451  ello12  15469  lo1bdd2  15477  elo12  15480  rlimconst  15497  isercoll  15621  climcau  15624  climbdd  15625  summolem2  15669  fsumconst  15743  o1fsum  15767  incexclem  15792  fprodconst  15934  bitsfzo  16395  dvdsmulgcd  16516  pc2dvds  16841  pcz  16843  pcadd  16851  pcfac  16861  vdwmc2  16941  vdwlem2  16944  vdwlem10  16952  vdw  16956  ramcl  16991  sbcie3s  17123  firest  17386  prdsval  17409  mreexd  17599  mreexexlemd  17601  iscat  17629  cidfval  17633  iscatd2  17638  catcocl  17642  catass  17643  catpropd  17666  cidpropd  17667  moni  17694  monpropd  17695  issubc  17793  subccocl  17803  funcco  17829  funcpropd  17860  fullpropd  17880  nati  17916  natpropd  17937  fucpropd  17938  xpcpropd  18165  curfuncf  18195  curf2ndf  18204  yonffthlem  18239  acsfiindd  18510  chnind  18578  chnso  18581  mgmhmeql  18675  sgrppropd  18690  mndpropd  18718  mhmeql  18785  smndex1mgm  18869  isgrpinv  18960  dfgrp3lem  19005  mhmmnd  19031  cycsubm  19168  cycsubmcom  19170  conjnmzb  19219  ghmqusnsg  19248  ghmquskerlem3  19252  ghmqusker  19253  gass  19267  symgextf  19383  dfod2  19530  gexdvds  19550  sylow3lem2  19594  efgredlem  19713  efgredeu  19718  ghmcmn  19797  oddvdssubg  19821  dprdfcntz  19983  pgpfaclem3  20051  gsumle  20111  isrng  20126  issrg  20160  isring  20209  dvdsrmul1  20340  issubdrg  20748  suborng  20844  islmhm2  21025  lmhmeql  21042  lssacsex  21134  rhmpreimaidl  21267  rhmqusnsg  21275  isphl  21618  uvcf1  21782  lindfmm  21817  sraassab  21858  issubassa2  21882  opsrval  22034  psdmul  22142  scmatmats  22486  smatvscl  22499  mdetunilem7  22593  gsummatr01lem4  22633  m2cpmfo  22731  pmatcollpw3fi1lem1  22761  pm2mpf1lem  22769  pm2mpf1  22774  mp2pm2mplem4  22784  pm2mpghm  22791  chfacfscmulfsupp  22834  chfacfpmmulfsupp  22838  cctop  22981  neiptoptop  23106  neiptopreu  23108  tgrest  23134  ordtrest2lem  23178  cnss1  23251  cncnp  23255  isnrm3  23334  uncmp  23378  cmpfi  23383  iunconn  23403  1stcrest  23428  subislly  23456  islly2  23459  cldllycmp  23470  lly1stc  23471  llycmpkgen2  23525  kgencn  23531  xkoccn  23594  ptcnplem  23596  pthaus  23613  txhaus  23622  txkgen  23627  xkohaus  23628  xkococnlem  23634  txconn  23664  regr1lem2  23715  kqreglem1  23716  reghmph  23768  nrmhmph  23769  trfil2  23862  ufileu  23894  flimopn  23950  flimcf  23957  fclscf  24000  ufilcmp  24007  cnpfcf  24016  cnextfun  24039  tgpmulg  24068  symgtgp  24081  tgpt0  24094  qustgplem  24096  ustex2sym  24192  ustex3sym  24193  trust  24204  restutop  24212  restutopopn  24213  ustuqtop4  24219  utop3cls  24226  utopreg  24227  cstucnd  24258  ucncn  24259  trcfilu  24268  neipcfilu  24270  ismet2  24308  metequiv2  24485  metcnp  24516  metcnp2  24517  metcnpi3  24521  txmetcnp  24522  metustto  24528  metustsym  24530  metust  24533  cfilucfil  24534  metuel2  24540  psmetutop  24542  restmetu  24545  metucn  24546  ngptgp  24611  tngngp  24629  nmoleub  24706  icccmp  24801  reconnlem2  24803  reconn  24804  xmetdcn2  24813  metdseq0  24830  metdscn  24832  elcncf2  24867  cncfmet  24886  cnheibor  24932  nmoleub2lem2  25093  nmoleub3  25096  cvsi  25107  iscfil2  25243  iscfil3  25250  cfilfcls  25251  equivcfil  25276  caubl  25285  bcthlem5  25305  pmltpc  25427  ovollb2  25466  ovoliunnul  25484  ovolicc2lem4  25497  volsup  25533  ioorf  25550  dyadss  25571  dyaddisjlem  25572  mbfposr  25629  cncombf  25635  mbflimsup  25643  i1fmulclem  25679  mbfi1fseqlem4  25695  iblss2  25783  ellimc2  25854  ellimc3  25856  dvnadd  25906  dvmptfsum  25952  dvferm1  25962  dvferm2  25964  fta1g  26145  plyeq0lem  26185  plydivex  26274  fta1  26285  aalioulem2  26310  aalioulem3  26311  ulmuni  26370  ulmbdd  26376  ulmdvlem3  26380  mtest  26382  abelthlem8  26417  efopn  26635  cxpmul2z  26668  cxpcn3lem  26724  jensen  26966  lgambdd  27014  lgamucov  27015  isppw2  27092  mersenne  27204  dchrelbas3  27215  dchrptlem1  27241  dchrpt  27244  lgsval2lem  27284  lgsdchrval  27331  lgsquad3  27364  2sqb  27409  2sqmo  27414  pntrsumbnd2  27544  pntpbnd  27565  pntibnd  27570  nosupno  27681  noinfno  27696  noetasuplem4  27714  noetalem1  27719  madebday  27906  cofcutr  27930  negsprop  28041  mulscom  28145  absmuls  28250  addonbday  28285  bdayfinbndlem1  28473  z12sge0  28489  remulscl  28508  tgjustr  28556  tglowdim1i  28583  tgbtwndiff  28588  tgifscgr  28590  iscgrglt  28596  tgcgrxfr  28600  lnext  28649  tgbtwnconn1lem3  28656  tgbtwnconn1  28657  legval  28666  legov  28667  legov2  28668  legtrd  28671  legtri3  28672  legso  28681  hlcgrex  28698  hlcgreu  28700  tglnne  28710  tglndim0  28711  tglineeltr  28713  tglinethru  28718  tglnne0  28722  tglnpt2  28723  colline  28731  tglowdim2l  28732  tglowdim2ln  28733  mirreu3  28736  miriso  28752  midexlem  28774  isperp  28794  perpcom  28795  perpneq  28796  isperp2  28797  footexALT  28800  footex  28803  colperpexlem3  28814  opphllem  28817  midex  28819  oppne3  28825  opptgdim2  28827  opphllem2  28830  opphllem3  28831  opphllem5  28833  opphllem6  28834  opphl  28836  outpasch  28837  lnopp2hpgb  28845  colopp  28851  lmieu  28866  trgcopy  28886  trgcopyeu  28888  iscgra1  28892  cgrane1  28894  cgrane2  28895  cgrane3  28896  cgrahl1  28898  cgrahl2  28899  cgracgr  28900  cgraswap  28902  cgracom  28904  cgratr  28905  flatcgra  28906  cgrabtwn  28908  cgrahl  28909  dfcgra2  28912  sacgr  28913  acopyeu  28916  inaghl  28927  cgrg3col4  28935  f1otrg  28953  f1otrge  28954  axsegcon  29010  axeuclidlem  29045  upgr1eopALT  29200  usgr1eop  29333  pthdepisspth  29818  wpthswwlks2on  30047  clwwlkf1  30134  clwwlknscsh  30147  2pthfrgr  30369  n4cyclfrgr  30376  frgrwopreglem5  30406  frgrwopreglem5ALT  30407  friendshipgt3  30483  smcnlem  30783  0lno  30876  ubthlem1  30956  ubthlem3  30958  chocunii  31387  occl  31390  5oalem1  31740  3oalem2  31749  nmopub2tALT  31995  nmfnleub2  32012  lnconi  32119  kbass5  32206  mdslmd1lem1  32411  mdslmd1lem2  32412  cdj1i  32519  opreu2reuALT  32561  disjabrex  32667  disjabrexf  32668  2ndresdju  32737  acunirnmpt  32747  acunirnmpt2  32748  acunirnmpt2f  32749  aciunf1lem  32750  fnpreimac  32758  fgreu  32759  suppovss  32769  xrge0infss  32848  xrofsup  32855  elq2  32900  fsumiunle  32917  sgnsub  32925  2exple2exp  32933  s3f1  33022  ccatf1  33024  ccatws1f1o  33026  swrdf1  33031  ressprs  33041  dfmgc2  33071  mgcf1o  33078  xrge0addgt0  33092  mndlrinvb  33100  mndlactf1  33101  mndlactfo  33102  mndractf1  33103  mndractfo  33104  mndlactf1o  33105  gsumfs2d  33137  suppgsumssiun  33148  gsumwun  33152  gsumwrd2dccatlem  33153  psgnfzto1stlem  33176  fzto1st1  33178  cycpmco2  33209  cycpmrn  33219  cyc3genpm  33228  cycpmconjs  33232  cyc3conja  33233  conjga  33246  fxpsubrg  33250  submarchi  33262  isarchi3  33263  archiabllem1  33269  archiabllem2a  33270  isarchiofld  33275  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem4  33321  elrgspnsubrunlem2  33324  erler  33341  rlocaddval  33344  rlocmulval  33345  rloccring  33346  rloc1r  33348  subrdom  33361  isdrng4  33371  fracfld  33384  imaslmod  33428  dvdsruasso  33460  unitprodclb  33464  nsgqusf1olem2  33489  lmhmqusker  33492  intlidl  33495  rhmquskerlem  33500  elrspunidl  33503  elrspunsn  33504  rhmimaidl  33507  prmidl2  33516  isprmidlc  33522  rhmpreimaprmidl  33526  qsidomlem2  33528  ssdifidllem  33531  ssdifidlprm  33533  mxidlprm  33545  ssmxidl  33549  opprqusplusg  33564  opprqusmulr  33566  qsdrngilem  33569  qsdrngi  33570  rsprprmprmidl  33597  rsprprmprmidlb  33598  rprmirred  33606  rprmirredb  33607  rprmdvdspow  33608  rprmdvdsprod  33609  1arithidom  33612  1arithufdlem2  33620  1arithufdlem3  33621  1arithufdlem4  33622  dfufd2lem  33624  dfufd2  33625  zringfrac  33629  deg1prod  33658  ply1dg3rt0irred  33659  r1plmhm  33685  r1pquslmic  33686  extvfvcl  33695  mplmulmvr  33698  mplvrpmga  33704  psrgsum  33707  psrmonprod  33711  esplyfval3  33731  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  exsslsb  33756  lindsunlem  33784  lindsun  33785  dimkerim  33787  fedgmullem1  33789  fedgmul  33791  dimlssid  33792  evls1fldgencl  33830  fldextrspunlsplem  33833  extdgfialg  33854  minplyirred  33871  fldext2chn  33888  constrmon  33904  constrconj  33905  constrfin  33906  constrelextdg2  33907  constrextdg2lem  33908  constrextdg2  33909  constrext2chnlem  33910  constrfiss  33911  cos9thpiminplylem2  33943  mdetpmtr1  33983  txomap  33994  qtophaus  33996  cmpcref  34010  zarclsun  34030  zarclssn  34033  zarcmplem  34041  pstmxmet  34057  sqsscirc1  34068  ordtrest2NEWlem  34082  ordtconnlem1  34084  pnfneige0  34111  lmxrge0  34112  lmdvg  34113  qqhval2  34142  esumcst  34223  esumrnmpt2  34228  esumfsup  34230  esumcvg  34246  esum2d  34253  esumiun  34254  sigaclfu2  34281  insiga  34297  ldsysgenld  34320  ldgenpisyslem1  34323  fiunelros  34334  measinb  34381  imambfm  34422  oms0  34457  omssubadd  34460  carsgclctunlem3  34480  eulerpartlemgvv  34536  dstrvprob  34632  signstfvneq0  34732  actfunsnrndisj  34765  reprinfz1  34782  breprexp  34793  afsval  34831  derangenlem  35369  sconnpi1  35437  cvmsss2  35472  cvmopnlem  35476  cvmlift3lem7  35523  msrval  35736  ifscgr  36242  cgrxfr  36253  btwnconn1lem13  36297  outsideofeu  36329  neibastop2lem  36558  weiunso  36664  irrdifflemf  37655  irrdiff  37656  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem14  37969  poimirlem22  37977  poimirlem29  37984  broucube  37989  heicant  37990  mblfinlem1  37992  itg2addnclem  38006  ftc1cnnc  38027  ftc1anclem7  38034  sstotbnd2  38109  equivtotbnd  38113  isbnd3  38119  ssbnd  38123  totbndbnd  38124  cntotbnd  38131  heibor1lem  38144  rrncmslem  38167  lssats  39472  lsat0cv  39493  lkrlss  39555  lfl1dim  39581  lfl1dim2N  39582  lkrpssN  39623  hlhgt2  39849  3dim2  39928  2dim  39930  lplncvrlvol  40076  paddasslem11  40290  pmapjat1  40313  2polssN  40375  pclfinclN  40410  pexmidlem8N  40437  lhpexle1lem  40467  4atex  40536  ltrnid  40595  trlator0  40631  cdlemg2cex  41051  tendodi1  41244  tendodi2  41245  diblss  41630  dihopelvalcpre  41708  dihatexv  41798  mapdval4N  42092  fldhmf1  42543  mndmolinv  42548  primrootscoprmpow  42552  posbezout  42553  primrootscoprbij2  42556  primrootspoweq0  42559  aks6d1c2p2  42572  hashscontpow  42575  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c5  42592  sticksstones8  42606  sticksstones12  42611  sticksstones22  42621  aks6d1c6lem3  42625  aks6d1c6isolem1  42627  unitscyglem3  42650  aks5  42657  sn-subeu  42873  sn-0tie0  42910  fiabv  42995  frlmsnic  42999  fsuppind  43037  prjspersym  43054  dffltz  43081  nna4b4nsq  43107  mzpindd  43192  mzpsubst  43194  mzpcompact2lem  43197  eldioph2b  43209  irrapxlem3  43270  irrapxlem5  43272  pellex  43281  pell1234qrdich  43307  pell14qrexpcl  43313  congabseq  43420  jm2.26a  43446  jm2.26lem3  43447  rmydioph  43460  lnrfg  43565  hbt  43576  cantnftermord  43766  cantnfresb  43770  cantnf2  43771  oawordex2  43772  omabs2  43778  tfsconcatfv  43787  tfsconcatrev  43794  ofoaass  43806  nadd2rabtr  43830  nadd1suc  43838  naddgeoa  43840  rfovcnvf1od  44449  clsk3nimkb  44485  ntrneiiso  44536  ntrneikb  44539  ntrneixb  44540  ntrneik3  44541  ntrneix3  44542  ntrneik13  44543  ntrneix13  44544  4an4132  44944  iunconnlem2  45379  modelaxrep  45426  fnchoice  45478  cncmpmax  45481  ssinc  45535  ssdec  45536  disjf1  45631  supxrge  45786  suplesup  45787  infxr  45814  infleinf  45819  unb2ltle  45861  rexabslelem  45864  uzub  45877  supminfxr  45910  climrec  46051  climsuse  46056  islptre  46067  addlimc  46094  0ellimcdiv  46095  limsuppnfdlem  46147  limsupub  46150  limsuppnflem  46156  limsupubuz  46159  climinf3  46162  limsupmnflem  46166  climxrre  46196  liminfreuzlem  46248  liminflimsupclim  46253  xlimliminflimsup  46308  icccncfext  46333  cncfiooicclem1  46339  fperdvper  46365  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvmptfprodlem  46390  dvmptfprod  46391  dvnprodlem2  46393  stoweidlem7  46453  stoweidlem34  46480  stoweidlem52  46498  stoweidlem60  46506  wallispilem3  46513  fourierdlem34  46587  fourierdlem38  46591  fourierdlem39  46592  fourierdlem48  46600  fourierdlem50  46602  fourierdlem51  46603  fourierdlem73  46625  fourierdlem76  46628  fourierdlem77  46629  fourierdlem80  46632  fourierdlem87  46639  fourierdlem103  46655  fourierdlem104  46656  etransclem32  46712  etransclem33  46713  sge0f1o  46828  sge0pr  46840  sge0isum  46873  iundjiun  46906  meaiininclem  46932  hoicvr  46994  pimdecfgtioo  47163  pimincfltioo  47164  preimageiingt  47166  preimaleiinlt  47167  smflimlem2  47218  smflimlem4  47220  smfmullem3  47239  smflimmpt  47256  smfinflem  47263  smfpimne2  47286  fsupdm  47288  finfdm  47292  cfsetsnfsetfo  47520  funressnbrafv2  47704  imasetpreimafvbijlemf1  47876  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbnd  48297  isuspgrim  48384  stgrusgra  48447  isubgr3stgrlem6  48459  2zlidl  48728  lindslinindsimp2  48951  snlindsntor  48959  lincresunit2  48966  islindeps2  48971  imaf1co  49642  imasubc3  49643  fucofvalg  49805  fuco21  49823  precofvalALT  49855  lanfval  50100  ranfval  50101