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  6316  fsnex  7261  soisoi  7306  f1o2ndf1  8104  fimaproj  8117  fprlem2  8283  tz7.49  8416  omabs  8618  cofon1  8639  naddssim  8652  omxpenlem  9047  fopwdom  9054  findcard3  9236  findcard3OLD  9237  frfi  9239  finsschain  9317  marypha1lem  9391  wemappo  9509  wdomtr  9535  cantnfp1  9641  ttrcltr  9676  harcard  9938  numacn  10009  infunsdom1  10172  sornom  10237  ssfin4  10270  fin1a2lem11  10370  fin1a2lem13  10372  fpwwe2lem12  10602  pwfseq  10624  mulcmpblnr  11031  00id  11356  addrid  11361  cnegex  11362  negeu  11418  add20  11697  ltmul12a  12045  lediv12a  12083  cru  12185  qextltlem  13169  xleadd1a  13220  xmullem  13231  xlemul1a  13255  ixxss12  13333  ioodisj  13450  fvf1tp  13758  fsuppmapnn0fz  13968  seqf1o  14015  mulexpz  14074  leexp1a  14147  faclbnd  14262  swrdswrdlem  14676  abs3lem  15312  rexico  15327  cau3lem  15328  rlim3  15471  ello12  15489  lo1bdd2  15497  elo12  15500  rlimconst  15517  isercoll  15641  climcau  15644  climbdd  15645  summolem2  15689  fsumconst  15763  o1fsum  15786  incexclem  15809  fprodconst  15951  bitsfzo  16412  dvdsmulgcd  16533  pc2dvds  16857  pcz  16859  pcadd  16867  pcfac  16877  vdwmc2  16957  vdwlem2  16960  vdwlem10  16968  vdw  16972  ramcl  17007  sbcie3s  17139  firest  17402  prdsval  17425  mreexd  17610  mreexexlemd  17612  iscat  17640  cidfval  17644  iscatd2  17649  catcocl  17653  catass  17654  catpropd  17677  cidpropd  17678  moni  17705  monpropd  17706  issubc  17804  subccocl  17814  funcco  17840  funcpropd  17871  fullpropd  17891  nati  17927  natpropd  17948  fucpropd  17949  xpcpropd  18176  curfuncf  18206  curf2ndf  18215  yonffthlem  18250  acsfiindd  18519  mgmhmeql  18650  sgrppropd  18665  mndpropd  18693  mhmeql  18760  smndex1mgm  18841  isgrpinv  18932  dfgrp3lem  18977  mhmmnd  19003  cycsubm  19141  cycsubmcom  19143  conjnmzb  19192  ghmqusnsg  19221  ghmquskerlem3  19225  ghmqusker  19226  gass  19240  symgextf  19354  dfod2  19501  gexdvds  19521  sylow3lem2  19565  efgredlem  19684  efgredeu  19689  ghmcmn  19768  oddvdssubg  19792  dprdfcntz  19954  pgpfaclem3  20022  isrng  20070  issrg  20104  isring  20153  dvdsrmul1  20285  issubdrg  20696  islmhm2  20952  lmhmeql  20969  lssacsex  21061  rhmpreimaidl  21194  rhmqusnsg  21202  isphl  21544  uvcf1  21708  lindfmm  21743  sraassab  21784  issubassa2  21808  opsrval  21960  psdmul  22060  scmatmats  22405  smatvscl  22418  mdetunilem7  22512  gsummatr01lem4  22552  m2cpmfo  22650  pmatcollpw3fi1lem1  22680  pm2mpf1lem  22688  pm2mpf1  22693  mp2pm2mplem4  22703  pm2mpghm  22710  chfacfscmulfsupp  22753  chfacfpmmulfsupp  22757  cctop  22900  neiptoptop  23025  neiptopreu  23027  tgrest  23053  ordtrest2lem  23097  cnss1  23170  cncnp  23174  isnrm3  23253  uncmp  23297  cmpfi  23302  iunconn  23322  1stcrest  23347  subislly  23375  islly2  23378  cldllycmp  23389  lly1stc  23390  llycmpkgen2  23444  kgencn  23450  xkoccn  23513  ptcnplem  23515  pthaus  23532  txhaus  23541  txkgen  23546  xkohaus  23547  xkococnlem  23553  txconn  23583  regr1lem2  23634  kqreglem1  23635  reghmph  23687  nrmhmph  23688  trfil2  23781  ufileu  23813  flimopn  23869  flimcf  23876  fclscf  23919  ufilcmp  23926  cnpfcf  23935  cnextfun  23958  tgpmulg  23987  symgtgp  24000  tgpt0  24013  qustgplem  24015  ustex2sym  24111  ustex3sym  24112  trust  24124  restutop  24132  restutopopn  24133  ustuqtop4  24139  utop3cls  24146  utopreg  24147  cstucnd  24178  ucncn  24179  trcfilu  24188  neipcfilu  24190  ismet2  24228  metequiv2  24405  metcnp  24436  metcnp2  24437  metcnpi3  24441  txmetcnp  24442  metustto  24448  metustsym  24450  metust  24453  cfilucfil  24454  metuel2  24460  psmetutop  24462  restmetu  24465  metucn  24466  ngptgp  24531  tngngp  24549  nmoleub  24626  icccmp  24721  reconnlem2  24723  reconn  24724  xmetdcn2  24733  metdseq0  24750  metdscn  24752  elcncf2  24790  cncfmet  24809  cnheibor  24861  nmoleub2lem2  25023  nmoleub3  25026  cvsi  25037  iscfil2  25173  iscfil3  25180  cfilfcls  25181  equivcfil  25206  caubl  25215  bcthlem5  25235  pmltpc  25358  ovollb2  25397  ovoliunnul  25415  ovolicc2lem4  25428  volsup  25464  ioorf  25481  dyadss  25502  dyaddisjlem  25503  mbfposr  25560  cncombf  25566  mbflimsup  25574  i1fmulclem  25610  mbfi1fseqlem4  25626  iblss2  25714  ellimc2  25785  ellimc3  25787  dvnadd  25838  dvmptfsum  25886  dvferm1  25896  dvferm2  25898  fta1g  26082  plyeq0lem  26122  plydivex  26212  fta1  26223  aalioulem2  26248  aalioulem3  26249  ulmuni  26308  ulmbdd  26314  ulmdvlem3  26318  mtest  26320  abelthlem8  26356  efopn  26574  cxpmul2z  26607  cxpcn3lem  26664  jensen  26906  lgambdd  26954  lgamucov  26955  isppw2  27032  mersenne  27145  dchrelbas3  27156  dchrptlem1  27182  dchrpt  27185  lgsval2lem  27225  lgsdchrval  27272  lgsquad3  27305  2sqb  27350  2sqmo  27355  pntrsumbnd2  27485  pntpbnd  27506  pntibnd  27511  nosupno  27622  noinfno  27637  noetasuplem4  27655  noetalem1  27660  madebday  27818  cofcutr  27839  negsprop  27948  mulscom  28049  absmuls  28153  zs12ge0  28349  remulscl  28360  tgjustr  28408  tglowdim1i  28435  tgbtwndiff  28440  tgifscgr  28442  iscgrglt  28448  tgcgrxfr  28452  lnext  28501  tgbtwnconn1lem3  28508  tgbtwnconn1  28509  legval  28518  legov  28519  legov2  28520  legtrd  28523  legtri3  28524  legso  28533  hlcgrex  28550  hlcgreu  28552  tglnne  28562  tglndim0  28563  tglineeltr  28565  tglinethru  28570  tglnne0  28574  tglnpt2  28575  colline  28583  tglowdim2l  28584  tglowdim2ln  28585  mirreu3  28588  miriso  28604  midexlem  28626  isperp  28646  perpcom  28647  perpneq  28648  isperp2  28649  footexALT  28652  footex  28655  colperpexlem3  28666  opphllem  28669  midex  28671  oppne3  28677  opptgdim2  28679  opphllem2  28682  opphllem3  28683  opphllem5  28685  opphllem6  28686  opphl  28688  outpasch  28689  lnopp2hpgb  28697  colopp  28703  lmieu  28718  trgcopy  28738  trgcopyeu  28740  iscgra1  28744  cgrane1  28746  cgrane2  28747  cgrane3  28748  cgrahl1  28750  cgrahl2  28751  cgracgr  28752  cgraswap  28754  cgracom  28756  cgratr  28757  flatcgra  28758  cgrabtwn  28760  cgrahl  28761  dfcgra2  28764  sacgr  28765  acopyeu  28768  inaghl  28779  cgrg3col4  28787  f1otrg  28805  f1otrge  28806  axsegcon  28861  axeuclidlem  28896  upgr1eopALT  29051  usgr1eop  29184  pthdepisspth  29672  wpthswwlks2on  29898  clwwlkf1  29985  clwwlknscsh  29998  2pthfrgr  30220  n4cyclfrgr  30227  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  friendshipgt3  30334  smcnlem  30633  0lno  30726  ubthlem1  30806  ubthlem3  30808  chocunii  31237  occl  31240  5oalem1  31590  3oalem2  31599  nmopub2tALT  31845  nmfnleub2  31862  lnconi  31969  kbass5  32056  mdslmd1lem1  32261  mdslmd1lem2  32262  cdj1i  32369  opreu2reuALT  32413  disjabrex  32518  disjabrexf  32519  2ndresdju  32580  acunirnmpt  32590  acunirnmpt2  32591  acunirnmpt2f  32592  aciunf1lem  32593  fnpreimac  32602  fgreu  32603  suppovss  32611  xrge0infss  32690  xrofsup  32697  elq2  32743  fsumiunle  32761  sgnsub  32769  2exple2exp  32777  s3f1  32875  ccatf1  32877  ccatws1f1o  32880  swrdf1  32885  ressprs  32897  dfmgc2  32929  mgcf1o  32936  chnind  32944  chnso  32947  xrge0addgt0  32965  mndlrinvb  32973  mndlactf1  32974  mndlactfo  32975  mndractf1  32976  mndractfo  32977  mndlactf1o  32978  gsumfs2d  33002  gsumwun  33012  gsumwrd2dccatlem  33013  gsumle  33045  psgnfzto1stlem  33064  fzto1st1  33066  cycpmco2  33097  cycpmrn  33107  cyc3genpm  33116  cycpmconjs  33120  cyc3conja  33121  conjga  33134  submarchi  33147  isarchi3  33148  archiabllem1  33154  archiabllem2a  33155  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem2  33206  erler  33223  rlocaddval  33226  rlocmulval  33227  rloccring  33228  rloc1r  33230  subrdom  33242  isdrng4  33252  fracfld  33265  suborng  33300  isarchiofld  33302  imaslmod  33331  dvdsruasso  33363  unitprodclb  33367  nsgqusf1olem2  33392  lmhmqusker  33395  intlidl  33398  rhmquskerlem  33403  elrspunidl  33406  elrspunsn  33407  rhmimaidl  33410  prmidl2  33419  isprmidlc  33425  rhmpreimaprmidl  33429  qsidomlem2  33431  ssdifidllem  33434  ssdifidlprm  33436  mxidlprm  33448  ssmxidl  33452  opprqusplusg  33467  opprqusmulr  33469  qsdrngilem  33472  qsdrngi  33473  rsprprmprmidl  33500  rsprprmprmidlb  33501  rprmirred  33509  rprmirredb  33510  rprmdvdspow  33511  rprmdvdsprod  33512  1arithidom  33515  1arithufdlem2  33523  1arithufdlem3  33524  1arithufdlem4  33525  dfufd2lem  33527  dfufd2  33528  zringfrac  33532  ply1dg3rt0irred  33558  r1plmhm  33582  r1pquslmic  33583  exsslsb  33599  lindsunlem  33627  lindsun  33628  dimkerim  33630  fedgmullem1  33632  fedgmul  33634  dimlssid  33635  evls1fldgencl  33672  fldextrspunlsplem  33675  minplyirred  33708  fldext2chn  33725  constrmon  33741  constrconj  33742  constrfin  33743  constrelextdg2  33744  constrextdg2lem  33745  constrextdg2  33746  constrext2chnlem  33747  constrfiss  33748  cos9thpiminplylem2  33780  mdetpmtr1  33820  txomap  33831  qtophaus  33833  cmpcref  33847  zarclsun  33867  zarclssn  33870  zarcmplem  33878  pstmxmet  33894  sqsscirc1  33905  ordtrest2NEWlem  33919  ordtconnlem1  33921  pnfneige0  33948  lmxrge0  33949  lmdvg  33950  qqhval2  33979  esumcst  34060  esumrnmpt2  34065  esumfsup  34067  esumcvg  34083  esum2d  34090  esumiun  34091  sigaclfu2  34118  insiga  34134  ldsysgenld  34157  ldgenpisyslem1  34160  fiunelros  34171  measinb  34218  imambfm  34260  oms0  34295  omssubadd  34298  carsgclctunlem3  34318  eulerpartlemgvv  34374  dstrvprob  34470  signstfvneq0  34570  actfunsnrndisj  34603  reprinfz1  34620  breprexp  34631  afsval  34669  derangenlem  35165  sconnpi1  35233  cvmsss2  35268  cvmopnlem  35272  cvmlift3lem7  35319  msrval  35532  ifscgr  36039  cgrxfr  36050  btwnconn1lem13  36094  outsideofeu  36126  neibastop2lem  36355  weiunso  36461  irrdifflemf  37320  irrdiff  37321  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem14  37635  poimirlem22  37643  poimirlem29  37650  broucube  37655  heicant  37656  mblfinlem1  37658  itg2addnclem  37672  ftc1cnnc  37693  ftc1anclem7  37700  sstotbnd2  37775  equivtotbnd  37779  isbnd3  37785  ssbnd  37789  totbndbnd  37790  cntotbnd  37797  heibor1lem  37810  rrncmslem  37833  lssats  39012  lsat0cv  39033  lkrlss  39095  lfl1dim  39121  lfl1dim2N  39122  lkrpssN  39163  hlhgt2  39390  3dim2  39469  2dim  39471  lplncvrlvol  39617  paddasslem11  39831  pmapjat1  39854  2polssN  39916  pclfinclN  39951  pexmidlem8N  39978  lhpexle1lem  40008  4atex  40077  ltrnid  40136  trlator0  40172  cdlemg2cex  40592  tendodi1  40785  tendodi2  40786  diblss  41171  dihopelvalcpre  41249  dihatexv  41339  mapdval4N  41633  fldhmf1  42085  mndmolinv  42090  primrootscoprmpow  42094  posbezout  42095  primrootscoprbij2  42098  primrootspoweq0  42101  aks6d1c2p2  42114  hashscontpow  42117  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5  42134  sticksstones8  42148  sticksstones12  42153  sticksstones22  42163  aks6d1c6lem3  42167  aks6d1c6isolem1  42169  unitscyglem3  42192  aks5  42199  sn-subeu  42422  sn-0tie0  42446  fiabv  42531  frlmsnic  42535  fsuppind  42585  prjspersym  42602  dffltz  42629  nna4b4nsq  42655  mzpindd  42741  mzpsubst  42743  mzpcompact2lem  42746  eldioph2b  42758  irrapxlem3  42819  irrapxlem5  42821  pellex  42830  pell1234qrdich  42856  pell14qrexpcl  42862  congabseq  42970  jm2.26a  42996  jm2.26lem3  42997  rmydioph  43010  lnrfg  43115  hbt  43126  cantnftermord  43316  cantnfresb  43320  cantnf2  43321  oawordex2  43322  omabs2  43328  tfsconcatfv  43337  tfsconcatrev  43344  ofoaass  43356  nadd2rabtr  43380  nadd1suc  43388  naddgeoa  43390  rfovcnvf1od  44000  clsk3nimkb  44036  ntrneiiso  44087  ntrneikb  44090  ntrneixb  44091  ntrneik3  44092  ntrneix3  44093  ntrneik13  44094  ntrneix13  44095  4an4132  44496  iunconnlem2  44931  modelaxrep  44978  fnchoice  45030  cncmpmax  45033  ssinc  45088  ssdec  45089  disjf1  45184  supxrge  45341  suplesup  45342  infxr  45370  infleinf  45375  unb2ltle  45418  rexabslelem  45421  uzub  45434  supminfxr  45467  climrec  45608  climsuse  45613  islptre  45624  addlimc  45653  0ellimcdiv  45654  limsuppnfdlem  45706  limsupub  45709  limsuppnflem  45715  limsupubuz  45718  climinf3  45721  limsupmnflem  45725  climxrre  45755  liminfreuzlem  45807  liminflimsupclim  45812  xlimliminflimsup  45867  icccncfext  45892  cncfiooicclem1  45898  fperdvper  45924  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvmptfprodlem  45949  dvmptfprod  45950  dvnprodlem2  45952  stoweidlem7  46012  stoweidlem34  46039  stoweidlem52  46057  stoweidlem60  46065  wallispilem3  46072  fourierdlem34  46146  fourierdlem38  46150  fourierdlem39  46151  fourierdlem48  46159  fourierdlem50  46161  fourierdlem51  46162  fourierdlem73  46184  fourierdlem76  46187  fourierdlem77  46188  fourierdlem80  46191  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  etransclem32  46271  etransclem33  46272  sge0f1o  46387  sge0pr  46399  sge0isum  46432  iundjiun  46465  meaiininclem  46491  pimdecfgtioo  46722  pimincfltioo  46723  preimageiingt  46725  preimaleiinlt  46726  smflimlem2  46777  smflimlem4  46779  smfmullem3  46798  smflimmpt  46815  smfinflem  46822  smfpimne2  46845  fsupdm  46847  finfdm  46851  cfsetsnfsetfo  47065  funressnbrafv2  47249  imasetpreimafvbijlemf1  47409  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbnd  47814  isuspgrim  47900  stgrusgra  47962  isubgr3stgrlem6  47974  2zlidl  48232  lindslinindsimp2  48456  snlindsntor  48464  lincresunit2  48471  islindeps2  48476  imaf1co  49148  imasubc3  49149  fucofvalg  49311  fuco21  49329  precofvalALT  49361  lanfval  49606  ranfval  49607