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  6343  fsnex  7291  soisoi  7336  f1o2ndf1  8135  fimaproj  8154  fprlem2  8322  tz7.49  8458  omabs  8663  cofon1  8684  naddssim  8698  omxpenlem  9100  fopwdom  9107  findcard3  9277  frfi  9279  finsschain  9351  marypha1lem  9428  wemappo  9546  wdomtr  9572  cantnfp1  9685  ttrcltr  9720  harcard  10062  numacn  10131  infunsdom1  10293  sornom  10358  ssfin4  10391  fin1a2lem11  10491  fin1a2lem13  10493  fpwwe2lem12  10730  pwfseq  10752  mulcmpblnr  11159  00id  11488  addrid  11493  cnegex  11494  negeu  11550  add20  11831  ltmul12a  12176  lediv12a  12213  cru  12315  qextltlem  13335  xleadd1a  13386  xmullem  13397  xlemul1a  13421  ixxss12  13499  ioodisj  13616  fvf1tp  13932  fsuppmapnn0fz  14142  seqf1o  14189  mulexpz  14248  leexp1a  14321  faclbnd  14437  ccatf1  14739  swrdf1  14803  swrdswrdlem  14857  s3rex  15106  sgnsub  15264  abs3lem  15511  rexico  15526  cau3lem  15527  rlim3  15670  ello12  15688  lo1bdd2  15696  elo12  15699  rlimconst  15716  isercoll  15840  climcau  15843  climbdd  15844  summolem2  15887  fsumconst  15961  o1fsum  15985  incexclem  16010  fprodconst  16150  bitsfzo  16610  dvdsmulgcd  16735  pc2dvds  17062  pcz  17064  pcadd  17072  pcfac  17082  vdwmc2  17162  vdwlem2  17165  vdwlem10  17173  vdw  17177  ramcl  17212  sbcie3s  17345  firest  17608  prdsval  17631  mreexd  17821  mreexexlemd  17823  iscat  17851  cidfval  17855  iscatd2  17860  catcocl  17864  catass  17865  catpropd  17888  cidpropd  17889  moni  17916  monpropd  17917  issubc  18015  subccocl  18025  funcco  18051  funcpropd  18082  fullpropd  18102  nati  18138  natpropd  18159  fucpropd  18160  xpcpropd  18387  curfuncf  18417  curf2ndf  18426  yonffthlem  18461  acsfiindd  18732  chnind  18800  chnso  18803  mgmhmeql  18910  sgrppropd  18925  mndpropd  18956  mhmeql  19027  smndex1mgm  19111  isgrpinv  19209  dfgrp3lem  19253  mhmmnd  19279  cycsubm  19422  cycsubmcom  19424  conjnmzb  19472  ghmqusnsg  19501  ghmquskerlem3  19505  ghmqusker  19506  gass  19520  symgextf  19636  dfod2  19783  gexdvds  19803  sylow3lem2  19847  efgredlem  19966  efgredeu  19971  ghmcmn  20050  oddvdssubg  20074  dprdfcntz  20236  pgpfaclem3  20304  gsumle  20364  isrng  20381  issrg  20419  isring  20468  dvdsrmul1  20604  isdrng4  20997  issubdrg  21042  suborng  21138  islmhm2  21318  lmhmeql  21335  lssacsex  21427  rhmpreimaidl  21576  rhmqusnsg  21586  prmidl2  21627  isprmidlc  21633  rhmpreimaprmidl  21640  qsidomlem2  21642  ssdifidllem  21645  ssdifidlprm  21647  isphl  21939  uvcf1  22103  lindfmm  22138  sraassab  22181  issubassa2  22205  opsrval  22360  psdmul  22492  scmatmats  22831  smatvscl  22844  mdetunilem7  22938  gsummatr01lem4  22978  matunitlindflem1  22999  matunitlindflem2  23000  m2cpmfo  23079  pmatcollpw3fi1lem1  23109  pm2mpf1lem  23117  pm2mpf1  23122  mp2pm2mplem4  23132  pm2mpghm  23139  chfacfscmulfsupp  23182  chfacfpmmulfsupp  23186  cctop  23329  neiptoptop  23454  neiptopreu  23456  tgrest  23482  ordtrest2lem  23526  cnss1  23599  cncnp  23603  isnrm3  23682  uncmp  23726  cmpfi  23731  iunconn  23751  1stcrest  23776  subislly  23805  islly2  23808  cldllycmp  23819  lly1stc  23820  llycmpkgen2  23874  kgencn  23880  xkoccn  23943  ptcnplem  23945  pthaus  23962  txhaus  23971  txkgen  23976  xkohaus  23977  xkococnlem  23983  txconn  24013  regr1lem2  24064  kqreglem1  24065  reghmph  24117  nrmhmph  24118  trfil2  24211  ufileu  24243  flimopn  24299  flimcf  24306  fclscf  24349  ufilcmp  24356  cnpfcf  24365  cnextfun  24388  tgpmulg  24417  symgtgp  24430  tgpt0  24443  qustgplem  24445  ustex2sym  24541  ustex3sym  24542  trust  24553  restutop  24561  restutopopn  24562  ustuqtop4  24568  utop3cls  24575  utopreg  24576  cstucnd  24607  ucncn  24608  trcfilu  24617  neipcfilu  24619  ismet2  24657  metequiv2  24834  metcnp  24865  metcnp2  24866  metcnpi3  24870  txmetcnp  24871  metustto  24877  metustsym  24879  metust  24882  cfilucfil  24883  metuel2  24889  psmetutop  24891  restmetu  24894  metucn  24895  ngptgp  24960  tngngp  24978  nmoleub  25055  icccmp  25150  reconnlem2  25152  reconn  25153  xmetdcn2  25162  metdseq0  25179  metdscn  25181  elcncf2  25216  cncfmet  25235  cnheibor  25281  nmoleub2lem2  25442  nmoleub3  25445  cvsi  25456  iscfil2  25592  iscfil3  25599  cfilfcls  25600  equivcfil  25625  caubl  25634  bcthlem5  25654  pmltpc  25776  ovollb2  25815  ovoliunnul  25833  ovolicc2lem4  25846  volsup  25882  ioorf  25899  dyadss  25920  dyaddisjlem  25921  mbfposr  25978  cncombf  25984  mbflimsup  25992  i1fmulclem  26028  mbfi1fseqlem4  26044  iblss2  26131  ellimc2  26202  ellimc3  26204  dvnadd  26254  dvmptfsum  26300  dvferm1  26310  dvferm2  26312  fta1g  26493  plyeq0lem  26534  plydivex  26623  fta1  26634  aalioulem2  26665  aalioulem3  26666  ulmuni  26724  ulmbdd  26730  ulmdvlem3  26734  mtest  26736  abelthlem8  26771  efopn  26991  cxpmul2z  27024  cxpcn3lem  27080  jensen  27321  lgambdd  27369  lgamucov  27370  isppw2  27447  mersenne  27559  dchrelbas3  27570  dchrptlem1  27596  dchrpt  27599  lgsval2lem  27639  lgsdchrval  27686  lgsquad3  27719  2sqb  27764  2sqmo  27769  pntrsumbnd2  27899  pntpbnd  27920  pntibnd  27925  nna4b4nsq  27995  nosupno  28065  noinfno  28080  noetasuplem4  28098  noetalem1  28103  madebday  28291  cofcutr  28315  negsprop  28426  mulscom  28530  absmuls  28635  addonbday  28670  bdayfinbndlem1  28858  z12sge0  28874  remulscl  28893  tgjustr  28941  tgsegconeu  28954  tglowdim1i  28969  tgbtwndiff  28974  tgifscgr  28976  iscgrglt  28982  tgcgrxfr  28986  lnext  29035  tgbtwnconn1lem3  29042  tgbtwnconn1  29043  legval  29052  legov  29053  legov2  29054  legtrd  29057  legtri3  29058  legso  29067  hlcgrex  29087  hlcgreu  29089  tglnne  29101  tglndim0  29102  tglineeltr  29104  tglinethru  29109  tglinesseq  29113  tglnne0  29114  colline  29123  tglowdim2l  29124  tglowdim2ln  29125  tglnpt2  29126  tglnpt3  29127  tglnpt4  29128  mirreu3  29131  miriso  29147  midexlem  29169  isperp  29192  perpcom  29193  perpneq  29194  isperp2  29195  footexALT  29198  footex  29201  colperpexlem3  29213  opphllem  29216  midex  29218  oppne3  29224  opptgdim2  29226  opphllem2  29229  opphllem3  29230  opphllem5  29232  opphllem6  29233  opphl  29235  outpasch  29238  lnopp2hpgb  29246  colopp  29252  plngrnssp  29262  lnincplng  29267  plngrotlem1  29270  plngrotlem3  29272  lnssplng  29275  plng3p  29280  lmieu  29294  trgcopy  29316  trgcopyeu  29318  iscgra1  29322  cgrane1  29324  cgrane2  29325  cgrane3  29326  cgrahl1  29328  cgrahl2  29329  cgracgr  29330  cgraswap  29332  cgracom  29334  cgratr  29335  zerocgra  29336  flatcgra  29337  cgrabtwn  29339  cgrahl  29340  dfcgra2  29343  sacgr  29344  acopyeu  29347  ragcgra  29348  cgrarag  29349  ragsupplcgra  29350  tgaaddcpbllem1  29354  tgaaddcpbllem3  29356  tgaaddcpbl  29357  inaghl  29369  cgrg3col4  29377  cgraer  29382  cgrabasimass  29383  angmgmaddeu1  29384  angmgmaddeu2  29385  angmgmaddeu3  29386  angmgmaddeu4  29387  angmgmaddeu5  29388  angmgmaddeu6  29389  angmgmaddeu7  29390  angmgmaddov2lem  29392  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmaddlid  29397  angmgmaddrid  29398  angmgm  29402  prlnghpg  29429  dfprlng2  29430  dfprlng3  29431  perpprlng  29433  prlngex  29434  prlngmolem1  29435  prlngmolem2  29436  prlngmo2  29439  prlngplngtr  29442  quadcgrprlng  29449  f1otrg  29453  f1otrge  29454  axsegcon  29510  axeuclidlem  29545  upgr1eopALT  29700  usgr1eop  29836  pthdepisspth  30326  wpthswwlks2on  30558  clwwlkf1  30645  clwwlknscsh  30658  2pthfrgr  30890  n4cyclfrgr  30897  frgrwopreglem5  30927  frgrwopreglem5ALT  30928  friendshipgt3  31004  smcnlem  31304  0lno  31397  ubthlem1  31477  ubthlem3  31479  chocunii  31908  occl  31911  5oalem1  32261  3oalem2  32270  nmopub2tALT  32516  nmfnleub2  32533  lnconi  32640  kbass5  32727  mdslmd1lem1  32932  mdslmd1lem2  32933  cdj1i  33040  cgrahlb  33052  opreu2reuALT  33120  disjabrex  33223  disjabrexf  33224  2ndresdju  33290  acunirnmpt  33300  acunirnmpt2  33301  acunirnmpt2f  33302  aciunf1lem  33303  fnpreimac  33311  fgreu  33312  suppovss  33321  xrge0infss  33398  xrofsup  33405  elq2  33449  fsumiunle  33466  2exple2exp  33471  s3f1  33557  ccatws1f1o  33560  ressprs  33573  dfmgc2  33603  mgcf1o  33610  xrge0addgt0  33624  mndlrinvb  33632  mndlactf1  33633  mndlactfo  33634  mndractf1  33635  mndractfo  33636  mndlactf1o  33637  gsumfs2d  33668  suppgsumssiun  33679  gsumwun  33683  gsumwrd2dccatlem  33684  psgnfzto1stlem  33707  fzto1st1  33709  cycpmco2  33740  cycpmrn  33750  cyc3genpm  33759  cycpmconjs  33763  cyc3conja  33764  conjga  33777  fxpsubrg  33781  submarchi  33793  isarchi3  33794  archiabllem1  33800  archiabllem2a  33801  isarchiofld  33806  elrgspnlem1  33849  elrgspnlem2  33850  elrgspnlem4  33852  elrgspnsubrunlem2  33855  erler  33872  rlocaddval  33876  rlocmulval  33877  rloccring  33878  rloc1r  33880  rlocisunit  33883  subrdom  33892  ricdomn1  33896  fracfld  33916  imaslmod  33960  dvdsruasso  33986  unitprodclb  33990  nsgqusf1olem2  34011  lmhmqusker  34014  intlidl  34016  rhmquskerlem  34021  elrspunidl  34024  elrspunsn  34025  rhmimaidl  34028  mxidlprm  34041  ssmxidl  34045  opprqusplusg  34059  opprqusmulr  34061  qsdrngilem  34064  qsdrngi  34065  drnglring  34070  dflring2  34071  dflringlem2  34073  rsprprmprmidl  34100  rsprprmprmidlb  34101  rprmirred  34109  rprmirredb  34110  rprmdvdspow  34111  rprmdvdsprod  34112  1arithidom  34115  1arithufdlem2  34123  1arithufdlem3  34124  1arithufdlem4  34125  dfufd2lem  34127  dfufd2  34128  zringfrac  34132  deg1prod  34161  ply1dg3rt0irred  34162  r1plmhm  34187  r1pquslmic  34188  0mplrim  34192  mplidomlem  34205  extvfvcl  34214  mplmulmvr  34217  mplvrpmga  34223  psrgsum  34226  psrmonprod  34230  esplyfval3  34250  esplyfval1  34251  esplyfvaln  34252  esplyind  34253  exsslsb  34275  lindsunlem  34302  lindsun  34303  dimkerim  34305  fedgmullem1  34307  fedgmul  34309  dimlssid  34310  evls1fldgencl  34348  fldextrspunlsplem  34351  extdgfialg  34372  minplyirred  34389  fldext2chn  34406  constrmon  34422  constrconj  34423  constrfin  34424  constrelextdg2  34425  constrextdg2lem  34426  constrextdg2  34427  constrext2chnlem  34428  constrfiss  34429  cos9thpiminplylem2  34461  mdetpmtr1  34501  txomap  34512  qtophaus  34514  cmpcref  34528  zarclsun  34548  zarclssn  34551  zarcmplem  34559  pstmxmet  34575  sqsscirc1  34586  ordtrest2NEWlem  34600  ordtconnlem1  34602  pnfneige0  34629  lmxrge0  34630  lmdvg  34631  qqhval2  34660  esumcst  34741  esumrnmpt2  34746  esumfsup  34748  esumcvg  34764  esum2d  34771  esumiun  34772  sigaclfu2  34799  insiga  34816  ldsysgenld  34839  ldgenpisyslem1  34842  fiunelros  34853  measinb  34900  imambfm  34940  oms0  34975  omssubadd  34978  carsgclctunlem3  34998  eulerpartlemgvv  35054  dstrvprob  35150  signstfvneq0  35247  actfunsnrndisj  35280  reprinfz1  35297  breprexp  35308  afsval  35349  j0ltalephlem  35946  derangenlem  36022  sconnpi1  36090  cvmsss2  36125  cvmopnlem  36129  cvmlift3lem7  36176  msrval  36389  ifscgr  36901  cgrxfr  36912  btwnconn1lem13  36956  outsideofeu  36988  nmulcom  37035  nmuladdss  37054  neibastop2lem  37240  weiunso  37346  mh-inf3f1  37421  irrdifflemf  38339  irrdiff  38340  poimirlem14  38645  poimirlem22  38653  poimirlem29  38660  broucube  38665  heicant  38666  mblfinlem1  38668  itg2addnclem  38682  ftc1cnnc  38703  ftc1anclem7  38710  sstotbnd2  38801  equivtotbnd  38805  isbnd3  38811  ssbnd  38815  totbndbnd  38816  cntotbnd  38823  heibor1lem  38836  rrncmslem  38859  lssats  40162  lsat0cv  40183  lkrlss  40245  lfl1dim  40271  lfl1dim2N  40272  lkrpssN  40313  hlhgt2  40539  3dim2  40618  2dim  40620  lplncvrlvol  40766  paddasslem11  40980  pmapjat1  41003  2polssN  41065  pclfinclN  41100  pexmidlem8N  41127  lhpexle1lem  41157  4atex  41226  ltrnid  41285  trlator0  41321  cdlemg2cex  41741  tendodi1  41934  tendodi2  41935  diblss  42320  dihopelvalcpre  42398  dihatexv  42488  mapdval4N  42782  fldhmf1  43233  mndmolinv  43238  primrootscoprmpow  43242  posbezout  43243  primrootscoprbij2  43246  primrootspoweq0  43249  aks6d1c2p2  43262  hashscontpow  43265  aks6d1c2lem4  43270  aks6d1c2  43273  aks6d1c5  43282  sticksstones8  43296  sticksstones12  43301  sticksstones22  43311  aks6d1c6lem3  43315  aks6d1c6isolem1  43317  unitscyglem3  43340  aks5  43347  sn-subeu  43571  sn-0tie0  43608  fiabv  43693  frlmsnic  43697  fsuppind  43711  prjspersym  43728  dffltz  43763  mzpindd  43850  mzpsubst  43852  mzpcompact2lem  43855  eldioph2b  43867  irrapxlem3  43924  irrapxlem5  43926  pellex  43935  pell1234qrdich  43961  pell14qrexpcl  43967  congabseq  44074  jm2.26a  44100  jm2.26lem3  44101  rmydioph  44114  lnrfg  44214  hbt  44225  cantnftermord  44415  cantnfresb  44419  cantnf2  44420  oawordex2  44421  omabs2  44427  tfsconcatfv  44436  tfsconcatrev  44443  ofoaass  44455  nadd2rabtr  44479  nadd1suc  44487  naddgeoa  44489  rfovcnvf1od  45097  clsk3nimkb  45133  ntrneiiso  45184  ntrneikb  45187  ntrneixb  45188  ntrneik3  45189  ntrneix3  45190  ntrneik13  45191  ntrneix13  45192  4an4132  45575  iunconnlem2  46010  modelaxrep  46064  fnchoice  46139  cncmpmax  46142  ssinc  46195  ssdec  46196  disjf1  46291  supxrge  46443  suplesup  46444  infxr  46471  infleinf  46476  unb2ltle  46518  rexabslelem  46521  uzub  46534  supminfxr  46567  climrec  46708  climsuse  46713  islptre  46724  addlimc  46751  0ellimcdiv  46752  limsuppnfdlem  46804  limsupub  46807  limsuppnflem  46813  limsupubuz  46816  climinf3  46819  limsupmnflem  46823  climxrre  46853  liminfreuzlem  46905  liminflimsupclim  46910  xlimliminflimsup  46965  icccncfext  46990  cncfiooicclem1  46996  fperdvper  47022  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  dvmptfprodlem  47047  dvmptfprod  47048  dvnprodlem2  47050  stoweidlem7  47110  stoweidlem34  47137  stoweidlem52  47155  stoweidlem60  47163  wallispilem3  47170  fourierdlem34  47244  fourierdlem38  47248  fourierdlem39  47249  fourierdlem48  47257  fourierdlem50  47259  fourierdlem51  47260  fourierdlem73  47282  fourierdlem76  47285  fourierdlem77  47286  fourierdlem80  47289  fourierdlem87  47296  fourierdlem103  47312  fourierdlem104  47313  etransclem32  47369  etransclem33  47370  sge0f1o  47485  sge0pr  47497  sge0isum  47530  iundjiun  47563  meaiininclem  47589  hoicvr  47651  pimdecfgtioo  47820  pimincfltioo  47821  preimageiingt  47823  preimaleiinlt  47824  smflimlem2  47875  smflimlem4  47877  smfmullem3  47896  smflimmpt  47913  smfinflem  47920  smfpimne2  47943  fsupdm  47945  finfdm  47949  cfsetsnfsetfo  48223  funressnbrafv2  48407  imasetpreimafvbijlemf1  48579  bgoldbtbndlem2  48997  bgoldbtbndlem3  48998  bgoldbtbnd  49000  isuspgrim  49087  stgrusgra  49150  isubgr3stgrlem6  49162  2zlidl  49430  lindslinindsimp2  49668  snlindsntor  49676  lincresunit2  49683  islindeps2  49688  imaf1co  50364  imasubc3  50365  fucofvalg  50533  fuco21  50551  precofvalALT  50596  lanfval  50889  ranfval  50890