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  6293  fsnex  7223  soisoi  7268  f1o2ndf1  8058  fimaproj  8071  fprlem2  8237  tz7.49  8370  omabs  8572  cofon1  8593  naddssim  8606  omxpenlem  8997  fopwdom  9004  findcard3  9173  frfi  9175  finsschain  9249  marypha1lem  9323  wemappo  9441  wdomtr  9467  cantnfp1  9577  ttrcltr  9612  harcard  9877  numacn  9946  infunsdom1  10109  sornom  10174  ssfin4  10207  fin1a2lem11  10307  fin1a2lem13  10309  fpwwe2lem12  10539  pwfseq  10561  mulcmpblnr  10968  00id  11294  addrid  11299  cnegex  11300  negeu  11356  add20  11635  ltmul12a  11983  lediv12a  12021  cru  12123  qextltlem  13107  xleadd1a  13158  xmullem  13169  xlemul1a  13193  ixxss12  13271  ioodisj  13388  fvf1tp  13699  fsuppmapnn0fz  13909  seqf1o  13956  mulexpz  14015  leexp1a  14088  faclbnd  14203  swrdswrdlem  14617  abs3lem  15252  rexico  15267  cau3lem  15268  rlim3  15411  ello12  15429  lo1bdd2  15437  elo12  15440  rlimconst  15457  isercoll  15581  climcau  15584  climbdd  15585  summolem2  15629  fsumconst  15703  o1fsum  15726  incexclem  15749  fprodconst  15891  bitsfzo  16352  dvdsmulgcd  16473  pc2dvds  16797  pcz  16799  pcadd  16807  pcfac  16817  vdwmc2  16897  vdwlem2  16900  vdwlem10  16908  vdw  16912  ramcl  16947  sbcie3s  17079  firest  17342  prdsval  17365  mreexd  17554  mreexexlemd  17556  iscat  17584  cidfval  17588  iscatd2  17593  catcocl  17597  catass  17598  catpropd  17621  cidpropd  17622  moni  17649  monpropd  17650  issubc  17748  subccocl  17758  funcco  17784  funcpropd  17815  fullpropd  17835  nati  17871  natpropd  17892  fucpropd  17893  xpcpropd  18120  curfuncf  18150  curf2ndf  18159  yonffthlem  18194  acsfiindd  18465  chnind  18533  chnso  18536  mgmhmeql  18630  sgrppropd  18645  mndpropd  18673  mhmeql  18740  smndex1mgm  18821  isgrpinv  18912  dfgrp3lem  18957  mhmmnd  18983  cycsubm  19120  cycsubmcom  19122  conjnmzb  19171  ghmqusnsg  19200  ghmquskerlem3  19204  ghmqusker  19205  gass  19219  symgextf  19335  dfod2  19482  gexdvds  19502  sylow3lem2  19546  efgredlem  19665  efgredeu  19670  ghmcmn  19749  oddvdssubg  19773  dprdfcntz  19935  pgpfaclem3  20003  gsumle  20063  isrng  20078  issrg  20112  isring  20161  dvdsrmul1  20293  issubdrg  20701  suborng  20797  islmhm2  20978  lmhmeql  20995  lssacsex  21087  rhmpreimaidl  21220  rhmqusnsg  21228  isphl  21571  uvcf1  21735  lindfmm  21770  sraassab  21811  issubassa2  21835  opsrval  21987  psdmul  22087  scmatmats  22432  smatvscl  22445  mdetunilem7  22539  gsummatr01lem4  22579  m2cpmfo  22677  pmatcollpw3fi1lem1  22707  pm2mpf1lem  22715  pm2mpf1  22720  mp2pm2mplem4  22730  pm2mpghm  22737  chfacfscmulfsupp  22780  chfacfpmmulfsupp  22784  cctop  22927  neiptoptop  23052  neiptopreu  23054  tgrest  23080  ordtrest2lem  23124  cnss1  23197  cncnp  23201  isnrm3  23280  uncmp  23324  cmpfi  23329  iunconn  23349  1stcrest  23374  subislly  23402  islly2  23405  cldllycmp  23416  lly1stc  23417  llycmpkgen2  23471  kgencn  23477  xkoccn  23540  ptcnplem  23542  pthaus  23559  txhaus  23568  txkgen  23573  xkohaus  23574  xkococnlem  23580  txconn  23610  regr1lem2  23661  kqreglem1  23662  reghmph  23714  nrmhmph  23715  trfil2  23808  ufileu  23840  flimopn  23896  flimcf  23903  fclscf  23946  ufilcmp  23953  cnpfcf  23962  cnextfun  23985  tgpmulg  24014  symgtgp  24027  tgpt0  24040  qustgplem  24042  ustex2sym  24138  ustex3sym  24139  trust  24150  restutop  24158  restutopopn  24159  ustuqtop4  24165  utop3cls  24172  utopreg  24173  cstucnd  24204  ucncn  24205  trcfilu  24214  neipcfilu  24216  ismet2  24254  metequiv2  24431  metcnp  24462  metcnp2  24463  metcnpi3  24467  txmetcnp  24468  metustto  24474  metustsym  24476  metust  24479  cfilucfil  24480  metuel2  24486  psmetutop  24488  restmetu  24491  metucn  24492  ngptgp  24557  tngngp  24575  nmoleub  24652  icccmp  24747  reconnlem2  24749  reconn  24750  xmetdcn2  24759  metdseq0  24776  metdscn  24778  elcncf2  24816  cncfmet  24835  cnheibor  24887  nmoleub2lem2  25049  nmoleub3  25052  cvsi  25063  iscfil2  25199  iscfil3  25206  cfilfcls  25207  equivcfil  25232  caubl  25241  bcthlem5  25261  pmltpc  25384  ovollb2  25423  ovoliunnul  25441  ovolicc2lem4  25454  volsup  25490  ioorf  25507  dyadss  25528  dyaddisjlem  25529  mbfposr  25586  cncombf  25592  mbflimsup  25600  i1fmulclem  25636  mbfi1fseqlem4  25652  iblss2  25740  ellimc2  25811  ellimc3  25813  dvnadd  25864  dvmptfsum  25912  dvferm1  25922  dvferm2  25924  fta1g  26108  plyeq0lem  26148  plydivex  26238  fta1  26249  aalioulem2  26274  aalioulem3  26275  ulmuni  26334  ulmbdd  26340  ulmdvlem3  26344  mtest  26346  abelthlem8  26382  efopn  26600  cxpmul2z  26633  cxpcn3lem  26690  jensen  26932  lgambdd  26980  lgamucov  26981  isppw2  27058  mersenne  27171  dchrelbas3  27182  dchrptlem1  27208  dchrpt  27211  lgsval2lem  27251  lgsdchrval  27298  lgsquad3  27331  2sqb  27376  2sqmo  27381  pntrsumbnd2  27511  pntpbnd  27532  pntibnd  27537  nosupno  27648  noinfno  27663  noetasuplem4  27681  noetalem1  27686  madebday  27851  cofcutr  27874  negsprop  27983  mulscom  28084  absmuls  28188  zs12ge0  28399  remulscl  28410  tgjustr  28458  tglowdim1i  28485  tgbtwndiff  28490  tgifscgr  28492  iscgrglt  28498  tgcgrxfr  28502  lnext  28551  tgbtwnconn1lem3  28558  tgbtwnconn1  28559  legval  28568  legov  28569  legov2  28570  legtrd  28573  legtri3  28574  legso  28583  hlcgrex  28600  hlcgreu  28602  tglnne  28612  tglndim0  28613  tglineeltr  28615  tglinethru  28620  tglnne0  28624  tglnpt2  28625  colline  28633  tglowdim2l  28634  tglowdim2ln  28635  mirreu3  28638  miriso  28654  midexlem  28676  isperp  28696  perpcom  28697  perpneq  28698  isperp2  28699  footexALT  28702  footex  28705  colperpexlem3  28716  opphllem  28719  midex  28721  oppne3  28727  opptgdim2  28729  opphllem2  28732  opphllem3  28733  opphllem5  28735  opphllem6  28736  opphl  28738  outpasch  28739  lnopp2hpgb  28747  colopp  28753  lmieu  28768  trgcopy  28788  trgcopyeu  28790  iscgra1  28794  cgrane1  28796  cgrane2  28797  cgrane3  28798  cgrahl1  28800  cgrahl2  28801  cgracgr  28802  cgraswap  28804  cgracom  28806  cgratr  28807  flatcgra  28808  cgrabtwn  28810  cgrahl  28811  dfcgra2  28814  sacgr  28815  acopyeu  28818  inaghl  28829  cgrg3col4  28837  f1otrg  28855  f1otrge  28856  axsegcon  28912  axeuclidlem  28947  upgr1eopALT  29102  usgr1eop  29235  pthdepisspth  29720  wpthswwlks2on  29949  clwwlkf1  30036  clwwlknscsh  30049  2pthfrgr  30271  n4cyclfrgr  30278  frgrwopreglem5  30308  frgrwopreglem5ALT  30309  friendshipgt3  30385  smcnlem  30684  0lno  30777  ubthlem1  30857  ubthlem3  30859  chocunii  31288  occl  31291  5oalem1  31641  3oalem2  31650  nmopub2tALT  31896  nmfnleub2  31913  lnconi  32020  kbass5  32107  mdslmd1lem1  32312  mdslmd1lem2  32313  cdj1i  32420  opreu2reuALT  32463  disjabrex  32569  disjabrexf  32570  2ndresdju  32638  acunirnmpt  32648  acunirnmpt2  32649  acunirnmpt2f  32650  aciunf1lem  32651  fnpreimac  32660  fgreu  32661  suppovss  32669  xrge0infss  32750  xrofsup  32757  elq2  32801  fsumiunle  32819  sgnsub  32827  2exple2exp  32835  s3f1  32935  ccatf1  32937  ccatws1f1o  32939  swrdf1  32944  ressprs  32954  dfmgc2  32984  mgcf1o  32991  xrge0addgt0  33005  mndlrinvb  33013  mndlactf1  33014  mndlactfo  33015  mndractf1  33016  mndractfo  33017  mndlactf1o  33018  gsumfs2d  33042  gsumwun  33052  gsumwrd2dccatlem  33053  psgnfzto1stlem  33076  fzto1st1  33078  cycpmco2  33109  cycpmrn  33119  cyc3genpm  33128  cycpmconjs  33132  cyc3conja  33133  conjga  33146  fxpsubrg  33150  submarchi  33162  isarchi3  33163  archiabllem1  33169  archiabllem2a  33170  isarchiofld  33175  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem4  33219  elrgspnsubrunlem2  33222  erler  33239  rlocaddval  33242  rlocmulval  33243  rloccring  33244  rloc1r  33246  subrdom  33258  isdrng4  33268  fracfld  33281  imaslmod  33325  dvdsruasso  33357  unitprodclb  33361  nsgqusf1olem2  33386  lmhmqusker  33389  intlidl  33392  rhmquskerlem  33397  elrspunidl  33400  elrspunsn  33401  rhmimaidl  33404  prmidl2  33413  isprmidlc  33419  rhmpreimaprmidl  33423  qsidomlem2  33425  ssdifidllem  33428  ssdifidlprm  33430  mxidlprm  33442  ssmxidl  33446  opprqusplusg  33461  opprqusmulr  33463  qsdrngilem  33466  qsdrngi  33467  rsprprmprmidl  33494  rsprprmprmidlb  33495  rprmirred  33503  rprmirredb  33504  rprmdvdspow  33505  rprmdvdsprod  33506  1arithidom  33509  1arithufdlem2  33517  1arithufdlem3  33518  1arithufdlem4  33519  dfufd2lem  33521  dfufd2  33522  zringfrac  33526  ply1dg3rt0irred  33553  r1plmhm  33577  r1pquslmic  33578  mplvrpmga  33582  exsslsb  33616  lindsunlem  33644  lindsun  33645  dimkerim  33647  fedgmullem1  33649  fedgmul  33651  dimlssid  33652  evls1fldgencl  33690  fldextrspunlsplem  33693  extdgfialg  33714  minplyirred  33731  fldext2chn  33748  constrmon  33764  constrconj  33765  constrfin  33766  constrelextdg2  33767  constrextdg2lem  33768  constrextdg2  33769  constrext2chnlem  33770  constrfiss  33771  cos9thpiminplylem2  33803  mdetpmtr1  33843  txomap  33854  qtophaus  33856  cmpcref  33870  zarclsun  33890  zarclssn  33893  zarcmplem  33901  pstmxmet  33917  sqsscirc1  33928  ordtrest2NEWlem  33942  ordtconnlem1  33944  pnfneige0  33971  lmxrge0  33972  lmdvg  33973  qqhval2  34002  esumcst  34083  esumrnmpt2  34088  esumfsup  34090  esumcvg  34106  esum2d  34113  esumiun  34114  sigaclfu2  34141  insiga  34157  ldsysgenld  34180  ldgenpisyslem1  34183  fiunelros  34194  measinb  34241  imambfm  34282  oms0  34317  omssubadd  34320  carsgclctunlem3  34340  eulerpartlemgvv  34396  dstrvprob  34492  signstfvneq0  34592  actfunsnrndisj  34625  reprinfz1  34642  breprexp  34653  afsval  34691  derangenlem  35222  sconnpi1  35290  cvmsss2  35325  cvmopnlem  35329  cvmlift3lem7  35376  msrval  35589  ifscgr  36095  cgrxfr  36106  btwnconn1lem13  36150  outsideofeu  36182  neibastop2lem  36411  weiunso  36517  irrdifflemf  37376  irrdiff  37377  matunitlindflem1  37662  matunitlindflem2  37663  poimirlem14  37680  poimirlem22  37688  poimirlem29  37695  broucube  37700  heicant  37701  mblfinlem1  37703  itg2addnclem  37717  ftc1cnnc  37738  ftc1anclem7  37745  sstotbnd2  37820  equivtotbnd  37824  isbnd3  37830  ssbnd  37834  totbndbnd  37835  cntotbnd  37842  heibor1lem  37855  rrncmslem  37878  lssats  39117  lsat0cv  39138  lkrlss  39200  lfl1dim  39226  lfl1dim2N  39227  lkrpssN  39268  hlhgt2  39494  3dim2  39573  2dim  39575  lplncvrlvol  39721  paddasslem11  39935  pmapjat1  39958  2polssN  40020  pclfinclN  40055  pexmidlem8N  40082  lhpexle1lem  40112  4atex  40181  ltrnid  40240  trlator0  40276  cdlemg2cex  40696  tendodi1  40889  tendodi2  40890  diblss  41275  dihopelvalcpre  41353  dihatexv  41443  mapdval4N  41737  fldhmf1  42189  mndmolinv  42194  primrootscoprmpow  42198  posbezout  42199  primrootscoprbij2  42202  primrootspoweq0  42205  aks6d1c2p2  42218  hashscontpow  42221  aks6d1c2lem4  42226  aks6d1c2  42229  aks6d1c5  42238  sticksstones8  42252  sticksstones12  42257  sticksstones22  42267  aks6d1c6lem3  42271  aks6d1c6isolem1  42273  unitscyglem3  42296  aks5  42303  sn-subeu  42526  sn-0tie0  42550  fiabv  42635  frlmsnic  42639  fsuppind  42689  prjspersym  42706  dffltz  42733  nna4b4nsq  42759  mzpindd  42844  mzpsubst  42846  mzpcompact2lem  42849  eldioph2b  42861  irrapxlem3  42922  irrapxlem5  42924  pellex  42933  pell1234qrdich  42959  pell14qrexpcl  42965  congabseq  43072  jm2.26a  43098  jm2.26lem3  43099  rmydioph  43112  lnrfg  43217  hbt  43228  cantnftermord  43418  cantnfresb  43422  cantnf2  43423  oawordex2  43424  omabs2  43430  tfsconcatfv  43439  tfsconcatrev  43446  ofoaass  43458  nadd2rabtr  43482  nadd1suc  43490  naddgeoa  43492  rfovcnvf1od  44102  clsk3nimkb  44138  ntrneiiso  44189  ntrneikb  44192  ntrneixb  44193  ntrneik3  44194  ntrneix3  44195  ntrneik13  44196  ntrneix13  44197  4an4132  44597  iunconnlem2  45032  modelaxrep  45079  fnchoice  45131  cncmpmax  45134  ssinc  45189  ssdec  45190  disjf1  45285  supxrge  45442  suplesup  45443  infxr  45470  infleinf  45475  unb2ltle  45518  rexabslelem  45521  uzub  45534  supminfxr  45567  climrec  45708  climsuse  45713  islptre  45724  addlimc  45751  0ellimcdiv  45752  limsuppnfdlem  45804  limsupub  45807  limsuppnflem  45813  limsupubuz  45816  climinf3  45819  limsupmnflem  45823  climxrre  45853  liminfreuzlem  45905  liminflimsupclim  45910  xlimliminflimsup  45965  icccncfext  45990  cncfiooicclem1  45996  fperdvper  46022  ioodvbdlimc1lem2  46035  ioodvbdlimc2lem  46037  dvmptfprodlem  46047  dvmptfprod  46048  dvnprodlem2  46050  stoweidlem7  46110  stoweidlem34  46137  stoweidlem52  46155  stoweidlem60  46163  wallispilem3  46170  fourierdlem34  46244  fourierdlem38  46248  fourierdlem39  46249  fourierdlem48  46257  fourierdlem50  46259  fourierdlem51  46260  fourierdlem73  46282  fourierdlem76  46285  fourierdlem77  46286  fourierdlem80  46289  fourierdlem87  46296  fourierdlem103  46312  fourierdlem104  46313  etransclem32  46369  etransclem33  46370  sge0f1o  46485  sge0pr  46497  sge0isum  46530  iundjiun  46563  meaiininclem  46589  pimdecfgtioo  46820  pimincfltioo  46821  preimageiingt  46823  preimaleiinlt  46824  smflimlem2  46875  smflimlem4  46877  smfmullem3  46896  smflimmpt  46913  smfinflem  46920  smfpimne2  46943  fsupdm  46945  finfdm  46949  cfsetsnfsetfo  47165  funressnbrafv2  47349  imasetpreimafvbijlemf1  47509  bgoldbtbndlem2  47911  bgoldbtbndlem3  47912  bgoldbtbnd  47914  isuspgrim  48001  stgrusgra  48064  isubgr3stgrlem6  48076  2zlidl  48345  lindslinindsimp2  48569  snlindsntor  48577  lincresunit2  48584  islindeps2  48589  imaf1co  49261  imasubc3  49262  fucofvalg  49424  fuco21  49442  precofvalALT  49474  lanfval  49719  ranfval  49720