Theorem simpllr 788

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 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad3antlr 744	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  frpomin  6361  fsnex  7314  soisoi  7359  f1o2ndf1  8160  fimaproj  8179  fprlem2  8347  tz7.49  8483  omabs  8688  cofon1  8709  naddssim  8723  omxpenlem  9125  fopwdom  9132  findcard3  9302  frfi  9304  finsschain  9376  marypha1lem  9452  wemappo  9570  wdomtr  9596  cantnfp1  9709  ttrcltr  9744  harcard  10086  numacn  10155  infunsdom1  10317  sornom  10382  ssfin4  10415  fin1a2lem11  10515  fin1a2lem13  10517  fpwwe2lem12  10754  pwfseq  10776  mulcmpblnr  11183  00id  11512  addrid  11517  cnegex  11518  negeu  11574  add20  11855  ltmul12a  12200  lediv12a  12237  cru  12339  qextltlem  13359  xleadd1a  13410  xmullem  13421  xlemul1a  13445  ixxss12  13523  ioodisj  13640  fvf1tp  13956  fsuppmapnn0fz  14166  seqf1o  14213  mulexpz  14272  leexp1a  14345  faclbnd  14461  ccatf1  14763  swrdf1  14827  swrdswrdlem  14881  s3rex  15130  sgnsub  15288  abs3lem  15535  rexico  15550  cau3lem  15551  rlim3  15694  ello12  15712  lo1bdd2  15720  elo12  15723  rlimconst  15740  isercoll  15864  climcau  15867  climbdd  15868  summolem2  15911  fsumconst  15985  o1fsum  16009  incexclem  16034  fprodconst  16174  bitsfzo  16634  dvdsmulgcd  16759  pc2dvds  17086  pcz  17088  pcadd  17096  pcfac  17106  vdwmc2  17186  vdwlem2  17189  vdwlem10  17197  vdw  17201  ramcl  17236  sbcie3s  17369  firest  17632  prdsval  17655  mreexd  17845  mreexexlemd  17847  iscat  17875  cidfval  17879  iscatd2  17884  catcocl  17888  catass  17889  catpropd  17912  cidpropd  17913  moni  17940  monpropd  17941  issubc  18039  subccocl  18049  funcco  18075  funcpropd  18106  fullpropd  18126  nati  18162  natpropd  18183  fucpropd  18184  xpcpropd  18411  curfuncf  18441  curf2ndf  18450  yonffthlem  18485  acsfiindd  18756  chnind  18824  chnso  18827  mgmhmeql  18934  sgrppropd  18949  mndpropd  18980  mhmeql  19051  smndex1mgm  19135  isgrpinv  19233  dfgrp3lem  19277  mhmmnd  19303  cycsubm  19446  cycsubmcom  19448  conjnmzb  19496  ghmqusnsg  19526  ghmquskerlem3  19530  ghmqusker  19531  gass  19545  symgextf  19661  dfod2  19808  gexdvds  19828  sylow3lem2  19872  efgredlem  19991  efgredeu  19996  ghmcmn  20075  oddvdssubg  20099  dprdfcntz  20261  pgpfaclem3  20329  gsumle  20389  isrng  20406  issrg  20444  isring  20493  dvdsrmul1  20629  isdrng4  21022  issubdrg  21067  suborng  21163  islmhm2  21343  lmhmeql  21360  lssacsex  21452  rhmpreimaidl  21601  rhmqusnsg  21611  prmidl2  21652  isprmidlc  21658  rhmpreimaprmidl  21665  qsidomlem2  21667  ssdifidllem  21670  ssdifidlprm  21672  isphl  21964  uvcf1  22128  lindfmm  22163  sraassab  22206  issubassa2  22230  opsrval  22385  psdmul  22517  scmatmats  22856  smatvscl  22869  mdetunilem7  22963  gsummatr01lem4  23003  matunitlindflem1  23024  matunitlindflem2  23025  m2cpmfo  23104  pmatcollpw3fi1lem1  23134  pm2mpf1lem  23142  pm2mpf1  23147  mp2pm2mplem4  23157  pm2mpghm  23164  chfacfscmulfsupp  23207  chfacfpmmulfsupp  23211  cctop  23354  neiptoptop  23479  neiptopreu  23481  tgrest  23507  ordtrest2lem  23551  cnss1  23624  cncnp  23628  isnrm3  23707  uncmp  23751  cmpfi  23756  iunconn  23776  1stcrest  23801  subislly  23830  islly2  23833  cldllycmp  23844  lly1stc  23845  llycmpkgen2  23899  kgencn  23905  xkoccn  23968  ptcnplem  23970  pthaus  23987  txhaus  23996  txkgen  24001  xkohaus  24002  xkococnlem  24008  txconn  24038  regr1lem2  24089  kqreglem1  24090  reghmph  24142  nrmhmph  24143  trfil2  24236  ufileu  24268  flimopn  24324  flimcf  24331  fclscf  24374  ufilcmp  24381  cnpfcf  24390  cnextfun  24413  tgpmulg  24442  symgtgp  24455  tgpt0  24468  qustgplem  24470  ustex2sym  24566  ustex3sym  24567  trust  24578  restutop  24586  restutopopn  24587  ustuqtop4  24593  utop3cls  24600  utopreg  24601  cstucnd  24632  ucncn  24633  trcfilu  24642  neipcfilu  24644  ismet2  24682  metequiv2  24859  metcnp  24890  metcnp2  24891  metcnpi3  24895  txmetcnp  24896  metustto  24902  metustsym  24904  metust  24907  cfilucfil  24908  metuel2  24914  psmetutop  24916  restmetu  24919  metucn  24920  ngptgp  24985  tngngp  25003  nmoleub  25080  icccmp  25175  reconnlem2  25177  reconn  25178  xmetdcn2  25187  metdseq0  25204  metdscn  25206  elcncf2  25241  cncfmet  25260  cnheibor  25306  nmoleub2lem2  25467  nmoleub3  25470  cvsi  25481  iscfil2  25617  iscfil3  25624  cfilfcls  25625  equivcfil  25650  caubl  25659  bcthlem5  25679  pmltpc  25801  ovollb2  25840  ovoliunnul  25858  ovolicc2lem4  25871  volsup  25907  ioorf  25924  dyadss  25945  dyaddisjlem  25946  mbfposr  26003  cncombf  26009  mbflimsup  26017  i1fmulclem  26053  mbfi1fseqlem4  26069  iblss2  26156  ellimc2  26227  ellimc3  26229  dvnadd  26279  dvmptfsum  26325  dvferm1  26335  dvferm2  26337  fta1g  26518  plyeq0lem  26559  plydivex  26648  fta1  26659  aalioulem2  26690  aalioulem3  26691  ulmuni  26749  ulmbdd  26755  ulmdvlem3  26759  mtest  26761  abelthlem8  26796  efopn  27016  cxpmul2z  27049  cxpcn3lem  27105  jensen  27346  lgambdd  27394  lgamucov  27395  isppw2  27472  mersenne  27584  dchrelbas3  27595  dchrptlem1  27621  dchrpt  27624  lgsval2lem  27664  lgsdchrval  27711  lgsquad3  27744  2sqb  27789  2sqmo  27794  pntrsumbnd2  27924  pntpbnd  27945  pntibnd  27950  nna4b4nsq  28020  nosupno  28090  noinfno  28105  noetasuplem4  28123  noetalem1  28128  madebday  28316  cofcutr  28340  negsprop  28451  mulscom  28555  absmuls  28660  addonbday  28695  bdayfinbndlem1  28883  z12sge0  28899  remulscl  28918  tgjustr  28966  tgsegconeu  28979  tglowdim1i  28994  tgbtwndiff  28999  tgifscgr  29001  iscgrglt  29007  tgcgrxfr  29011  lnext  29060  tgbtwnconn1lem3  29067  tgbtwnconn1  29068  legval  29077  legov  29078  legov2  29079  legtrd  29082  legtri3  29083  legso  29092  hlcgrex  29112  hlcgreu  29114  tglnne  29126  tglndim0  29127  tglineeltr  29129  tglinethru  29134  tglinesseq  29138  tglnne0  29139  colline  29148  tglowdim2l  29149  tglowdim2ln  29150  tglnpt2  29151  tglnpt3  29152  tglnpt4  29153  mirreu3  29156  miriso  29172  midexlem  29194  isperp  29217  perpcom  29218  perpneq  29219  isperp2  29220  footexALT  29223  footex  29226  colperpexlem3  29238  opphllem  29241  midex  29243  oppne3  29249  opptgdim2  29251  opphllem2  29254  opphllem3  29255  opphllem5  29257  opphllem6  29258  opphl  29260  outpasch  29263  lnopp2hpgb  29271  colopp  29277  plngrnssp  29287  lnincplng  29292  plngrotlem1  29295  plngrotlem3  29297  lnssplng  29300  plng3p  29305  lmieu  29319  trgcopy  29341  trgcopyeu  29343  iscgra1  29347  cgrane1  29349  cgrane2  29350  cgrane3  29351  cgrahl1  29353  cgrahl2  29354  cgracgr  29355  cgraswap  29357  cgracom  29359  cgratr  29360  zerocgra  29361  flatcgra  29362  cgrabtwn  29364  cgrahl  29365  dfcgra2  29368  sacgr  29369  acopyeu  29372  ragcgra  29373  cgrarag  29374  ragsupplcgra  29375  tgaaddcpbllem1  29379  tgaaddcpbllem3  29381  tgaaddcpbl  29382  inaghl  29394  cgrg3col4  29402  cgraer  29407  cgrabasimass  29408  angmgmaddeu1  29409  angmgmaddeu2  29410  angmgmaddeu3  29411  angmgmaddeu4  29412  angmgmaddeu5  29413  angmgmaddeu6  29414  angmgmaddeu7  29415  angmgmaddov2lem  29417  angmgmaddcpbl  29420  angmgmaddcl  29421  angmgmaddlid  29422  angmgmaddrid  29423  angmgm  29427  prlnghpg  29454  dfprlng2  29455  dfprlng3  29456  perpprlng  29458  prlngex  29459  prlngmolem1  29460  prlngmolem2  29461  prlngmo2  29464  prlngplngtr  29467  quadcgrprlng  29474  f1otrg  29478  f1otrge  29479  axsegcon  29535  axeuclidlem  29570  upgr1eopALT  29725  usgr1eop  29861  pthdepisspth  30351  wpthswwlks2on  30583  clwwlkf1  30670  clwwlknscsh  30683  2pthfrgr  30915  n4cyclfrgr  30922  frgrwopreglem5  30952  frgrwopreglem5ALT  30953  friendshipgt3  31029  smcnlem  31329  0lno  31422  ubthlem1  31502  ubthlem3  31504  chocunii  31933  occl  31936  5oalem1  32286  3oalem2  32295  nmopub2tALT  32541  nmfnleub2  32558  lnconi  32665  kbass5  32752  mdslmd1lem1  32957  mdslmd1lem2  32958  cdj1i  33065  cgrahlb  33077  opreu2reuALT  33145  disjabrex  33248  disjabrexf  33249  2ndresdju  33315  acunirnmpt  33325  acunirnmpt2  33326  acunirnmpt2f  33327  aciunf1lem  33328  fnpreimac  33336  fgreu  33337  suppovss  33345  xrge0infss  33422  xrofsup  33429  elq2  33473  fsumiunle  33490  2exple2exp  33495  s3f1  33581  ccatws1f1o  33584  ressprs  33597  dfmgc2  33627  mgcf1o  33634  xrge0addgt0  33648  mndlrinvb  33656  mndlactf1  33657  mndlactfo  33658  mndractf1  33659  mndractfo  33660  mndlactf1o  33661  gsumfs2d  33692  suppgsumssiun  33703  gsumwun  33707  gsumwrd2dccatlem  33708  psgnfzto1stlem  33731  fzto1st1  33733  cycpmco2  33764  cycpmrn  33774  cyc3genpm  33783  cycpmconjs  33787  cyc3conja  33788  conjga  33801  fxpsubrg  33805  submarchi  33817  isarchi3  33818  archiabllem1  33824  archiabllem2a  33825  isarchiofld  33830  elrgspnlem1  33873  elrgspnlem2  33874  elrgspnlem4  33876  elrgspnsubrunlem2  33879  erler  33896  rlocaddval  33900  rlocmulval  33901  rloccring  33902  rloc1r  33904  rlocisunit  33907  subrdom  33916  ricdomn1  33920  fracfld  33940  imaslmod  33984  dvdsruasso  34010  unitprodclb  34014  nsgqusf1olem2  34035  lmhmqusker  34038  intlidl  34040  rhmquskerlem  34045  elrspunidl  34048  elrspunsn  34049  rhmimaidl  34052  mxidlprm  34065  ssmxidl  34069  opprqusplusg  34083  opprqusmulr  34085  qsdrngilem  34088  qsdrngi  34089  drnglring  34094  dflring2  34095  dflringlem2  34097  rsprprmprmidl  34124  rsprprmprmidlb  34125  rprmirred  34133  rprmirredb  34134  rprmdvdspow  34135  rprmdvdsprod  34136  1arithidom  34139  1arithufdlem2  34147  1arithufdlem3  34148  1arithufdlem4  34149  dfufd2lem  34151  dfufd2  34152  zringfrac  34156  deg1prod  34185  ply1dg3rt0irred  34186  r1plmhm  34211  r1pquslmic  34212  0mplrim  34216  mplidomlem  34229  extvfvcl  34238  mplmulmvr  34241  mplvrpmga  34247  psrgsum  34250  psrmonprod  34254  esplyfval3  34274  esplyfval1  34275  esplyfvaln  34276  esplyind  34277  exsslsb  34299  lindsunlem  34326  lindsun  34327  dimkerim  34329  fedgmullem1  34331  fedgmul  34333  dimlssid  34334  evls1fldgencl  34372  fldextrspunlsplem  34375  extdgfialg  34396  minplyirred  34413  fldext2chn  34430  constrmon  34446  constrconj  34447  constrfin  34448  constrelextdg2  34449  constrextdg2lem  34450  constrextdg2  34451  constrext2chnlem  34452  constrfiss  34453  cos9thpiminplylem2  34485  mdetpmtr1  34525  txomap  34536  qtophaus  34538  cmpcref  34552  zarclsun  34572  zarclssn  34575  zarcmplem  34583  pstmxmet  34599  sqsscirc1  34610  ordtrest2NEWlem  34624  ordtconnlem1  34626  pnfneige0  34653  lmxrge0  34654  lmdvg  34655  qqhval2  34684  esumcst  34765  esumrnmpt2  34770  esumfsup  34772  esumcvg  34788  esum2d  34795  esumiun  34796  sigaclfu2  34823  insiga  34840  ldsysgenld  34863  ldgenpisyslem1  34866  fiunelros  34877  measinb  34924  imambfm  34964  oms0  34999  omssubadd  35002  carsgclctunlem3  35022  eulerpartlemgvv  35078  dstrvprob  35174  signstfvneq0  35271  actfunsnrndisj  35304  reprinfz1  35321  breprexp  35332  afsval  35373  j0ltalephlem  36007  dfk12  36012  dfk22  36013  dfk32  36014  derangenlem  36103  sconnpi1  36171  cvmsss2  36206  cvmopnlem  36210  cvmlift3lem7  36257  msrval  36470  ifscgr  36987  cgrxfr  36998  btwnconn1lem13  37042  outsideofeu  37074  nmulcom  37121  nmuladdss  37140  neibastop2lem  37326  weiunso  37432  mh-inf3f1  37507  irrdifflemf  38438  irrdiff  38439  poimirlem14  38744  poimirlem22  38752  poimirlem29  38759  broucube  38764  heicant  38765  mblfinlem1  38767  itg2addnclem  38781  ftc1cnnc  38802  ftc1anclem7  38809  sstotbnd2  38900  equivtotbnd  38904  isbnd3  38910  ssbnd  38914  totbndbnd  38915  cntotbnd  38922  heibor1lem  38935  rrncmslem  38958  lssats  40261  lsat0cv  40282  lkrlss  40344  lfl1dim  40370  lfl1dim2N  40371  lkrpssN  40412  hlhgt2  40638  3dim2  40717  2dim  40719  lplncvrlvol  40865  paddasslem11  41079  pmapjat1  41102  2polssN  41164  pclfinclN  41199  pexmidlem8N  41226  lhpexle1lem  41256  4atex  41325  ltrnid  41384  trlator0  41420  cdlemg2cex  41840  tendodi1  42033  tendodi2  42034  diblss  42419  dihopelvalcpre  42497  dihatexv  42587  mapdval4N  42881  fldhmf1  43332  mndmolinv  43337  primrootscoprmpow  43341  posbezout  43342  primrootscoprbij2  43345  primrootspoweq0  43348  aks6d1c2p2  43361  hashscontpow  43364  aks6d1c2lem4  43369  aks6d1c2  43372  aks6d1c5  43381  sticksstones8  43395  sticksstones12  43400  sticksstones22  43410  aks6d1c6lem3  43414  aks6d1c6isolem1  43416  unitscyglem3  43439  aks5  43446  sn-subeu  43671  sn-0tie0  43708  fiabv  43793  frlmsnic  43797  fsuppind  43811  prjspersym  43828  dffltz  43863  mzpindd  43950  mzpsubst  43952  mzpcompact2lem  43955  eldioph2b  43967  irrapxlem3  44024  irrapxlem5  44026  pellex  44035  pell1234qrdich  44061  pell14qrexpcl  44067  congabseq  44174  jm2.26a  44200  jm2.26lem3  44201  rmydioph  44214  lnrfg  44313  hbt  44324  cantnftermord  44514  cantnfresb  44518  cantnf2  44519  oawordex2  44520  omabs2  44526  tfsconcatfv  44535  tfsconcatrev  44542  ofoaass  44554  nadd2rabtr  44578  nadd1suc  44586  naddgeoa  44588  rfovcnvf1od  45196  clsk3nimkb  45232  ntrneiiso  45283  ntrneikb  45286  ntrneixb  45287  ntrneik3  45288  ntrneix3  45289  ntrneik13  45290  ntrneix13  45291  4an4132  45673  iunconnlem2  46108  modelaxrep  46166  fnchoice  46251  cncmpmax  46254  ssinc  46307  ssdec  46308  disjf1  46403  supxrge  46555  suplesup  46556  infxr  46583  infleinf  46588  unb2ltle  46630  rexabslelem  46633  uzub  46646  supminfxr  46679  climrec  46820  climsuse  46825  islptre  46836  addlimc  46863  0ellimcdiv  46864  limsuppnfdlem  46916  limsupub  46919  limsuppnflem  46925  limsupubuz  46928  climinf3  46931  limsupmnflem  46935  climxrre  46965  liminfreuzlem  47017  liminflimsupclim  47022  xlimliminflimsup  47077  icccncfext  47102  cncfiooicclem1  47108  fperdvper  47134  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  dvmptfprodlem  47159  dvmptfprod  47160  dvnprodlem2  47162  stoweidlem7  47222  stoweidlem34  47249  stoweidlem52  47267  stoweidlem60  47275  wallispilem3  47282  fourierdlem34  47356  fourierdlem38  47360  fourierdlem39  47361  fourierdlem48  47369  fourierdlem50  47371  fourierdlem51  47372  fourierdlem73  47394  fourierdlem76  47397  fourierdlem77  47398  fourierdlem80  47401  fourierdlem87  47408  fourierdlem103  47424  fourierdlem104  47425  etransclem32  47481  etransclem33  47482  sge0f1o  47597  sge0pr  47609  sge0isum  47642  iundjiun  47675  meaiininclem  47701  hoicvr  47763  pimdecfgtioo  47932  pimincfltioo  47933  preimageiingt  47935  preimaleiinlt  47936  smflimlem2  47987  smflimlem4  47989  smfmullem3  48008  smflimmpt  48025  smfinflem  48032  smfpimne2  48055  fsupdm  48057  finfdm  48061  cfsetsnfsetfo  48335  funressnbrafv2  48519  imasetpreimafvbijlemf1  48691  bgoldbtbndlem2  49109  bgoldbtbndlem3  49110  bgoldbtbnd  49112  isuspgrim  49199  stgrusgra  49262  isubgr3stgrlem6  49274  2zlidl  49542  lindslinindsimp2  49780  snlindsntor  49788  lincresunit2  49795  islindeps2  49800  imaf1co  50476  imasubc3  50477  fucofvalg  50645  fuco21  50663  precofvalALT  50708  lanfval  51001  ranfval  51002