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  6287  fsnex  7217  soisoi  7262  f1o2ndf1  8052  fimaproj  8065  fprlem2  8231  tz7.49  8364  omabs  8566  cofon1  8587  naddssim  8600  omxpenlem  8991  fopwdom  8998  findcard3  9167  frfi  9169  finsschain  9243  marypha1lem  9317  wemappo  9435  wdomtr  9461  cantnfp1  9571  ttrcltr  9606  harcard  9868  numacn  9937  infunsdom1  10100  sornom  10165  ssfin4  10198  fin1a2lem11  10298  fin1a2lem13  10300  fpwwe2lem12  10530  pwfseq  10552  mulcmpblnr  10959  00id  11285  addrid  11290  cnegex  11291  negeu  11347  add20  11626  ltmul12a  11974  lediv12a  12012  cru  12114  qextltlem  13098  xleadd1a  13149  xmullem  13160  xlemul1a  13184  ixxss12  13262  ioodisj  13379  fvf1tp  13690  fsuppmapnn0fz  13900  seqf1o  13947  mulexpz  14006  leexp1a  14079  faclbnd  14194  swrdswrdlem  14608  abs3lem  15243  rexico  15258  cau3lem  15259  rlim3  15402  ello12  15420  lo1bdd2  15428  elo12  15431  rlimconst  15448  isercoll  15572  climcau  15575  climbdd  15576  summolem2  15620  fsumconst  15694  o1fsum  15717  incexclem  15740  fprodconst  15882  bitsfzo  16343  dvdsmulgcd  16464  pc2dvds  16788  pcz  16790  pcadd  16798  pcfac  16808  vdwmc2  16888  vdwlem2  16891  vdwlem10  16899  vdw  16903  ramcl  16938  sbcie3s  17070  firest  17333  prdsval  17356  mreexd  17545  mreexexlemd  17547  iscat  17575  cidfval  17579  iscatd2  17584  catcocl  17588  catass  17589  catpropd  17612  cidpropd  17613  moni  17640  monpropd  17641  issubc  17739  subccocl  17749  funcco  17775  funcpropd  17806  fullpropd  17826  nati  17862  natpropd  17883  fucpropd  17884  xpcpropd  18111  curfuncf  18141  curf2ndf  18150  yonffthlem  18185  acsfiindd  18456  chnind  18524  chnso  18527  mgmhmeql  18621  sgrppropd  18636  mndpropd  18664  mhmeql  18731  smndex1mgm  18812  isgrpinv  18903  dfgrp3lem  18948  mhmmnd  18974  cycsubm  19112  cycsubmcom  19114  conjnmzb  19163  ghmqusnsg  19192  ghmquskerlem3  19196  ghmqusker  19197  gass  19211  symgextf  19327  dfod2  19474  gexdvds  19494  sylow3lem2  19538  efgredlem  19657  efgredeu  19662  ghmcmn  19741  oddvdssubg  19765  dprdfcntz  19927  pgpfaclem3  19995  gsumle  20055  isrng  20070  issrg  20104  isring  20153  dvdsrmul1  20285  issubdrg  20693  suborng  20789  islmhm2  20970  lmhmeql  20987  lssacsex  21079  rhmpreimaidl  21212  rhmqusnsg  21220  isphl  21563  uvcf1  21727  lindfmm  21762  sraassab  21803  issubassa2  21827  opsrval  21979  psdmul  22079  scmatmats  22424  smatvscl  22437  mdetunilem7  22531  gsummatr01lem4  22571  m2cpmfo  22669  pmatcollpw3fi1lem1  22699  pm2mpf1lem  22707  pm2mpf1  22712  mp2pm2mplem4  22722  pm2mpghm  22729  chfacfscmulfsupp  22772  chfacfpmmulfsupp  22776  cctop  22919  neiptoptop  23044  neiptopreu  23046  tgrest  23072  ordtrest2lem  23116  cnss1  23189  cncnp  23193  isnrm3  23272  uncmp  23316  cmpfi  23321  iunconn  23341  1stcrest  23366  subislly  23394  islly2  23397  cldllycmp  23408  lly1stc  23409  llycmpkgen2  23463  kgencn  23469  xkoccn  23532  ptcnplem  23534  pthaus  23551  txhaus  23560  txkgen  23565  xkohaus  23566  xkococnlem  23572  txconn  23602  regr1lem2  23653  kqreglem1  23654  reghmph  23706  nrmhmph  23707  trfil2  23800  ufileu  23832  flimopn  23888  flimcf  23895  fclscf  23938  ufilcmp  23945  cnpfcf  23954  cnextfun  23977  tgpmulg  24006  symgtgp  24019  tgpt0  24032  qustgplem  24034  ustex2sym  24130  ustex3sym  24131  trust  24142  restutop  24150  restutopopn  24151  ustuqtop4  24157  utop3cls  24164  utopreg  24165  cstucnd  24196  ucncn  24197  trcfilu  24206  neipcfilu  24208  ismet2  24246  metequiv2  24423  metcnp  24454  metcnp2  24455  metcnpi3  24459  txmetcnp  24460  metustto  24466  metustsym  24468  metust  24471  cfilucfil  24472  metuel2  24478  psmetutop  24480  restmetu  24483  metucn  24484  ngptgp  24549  tngngp  24567  nmoleub  24644  icccmp  24739  reconnlem2  24741  reconn  24742  xmetdcn2  24751  metdseq0  24768  metdscn  24770  elcncf2  24808  cncfmet  24827  cnheibor  24879  nmoleub2lem2  25041  nmoleub3  25044  cvsi  25055  iscfil2  25191  iscfil3  25198  cfilfcls  25199  equivcfil  25224  caubl  25233  bcthlem5  25253  pmltpc  25376  ovollb2  25415  ovoliunnul  25433  ovolicc2lem4  25446  volsup  25482  ioorf  25499  dyadss  25520  dyaddisjlem  25521  mbfposr  25578  cncombf  25584  mbflimsup  25592  i1fmulclem  25628  mbfi1fseqlem4  25644  iblss2  25732  ellimc2  25803  ellimc3  25805  dvnadd  25856  dvmptfsum  25904  dvferm1  25914  dvferm2  25916  fta1g  26100  plyeq0lem  26140  plydivex  26230  fta1  26241  aalioulem2  26266  aalioulem3  26267  ulmuni  26326  ulmbdd  26332  ulmdvlem3  26336  mtest  26338  abelthlem8  26374  efopn  26592  cxpmul2z  26625  cxpcn3lem  26682  jensen  26924  lgambdd  26972  lgamucov  26973  isppw2  27050  mersenne  27163  dchrelbas3  27174  dchrptlem1  27200  dchrpt  27203  lgsval2lem  27243  lgsdchrval  27290  lgsquad3  27323  2sqb  27368  2sqmo  27373  pntrsumbnd2  27503  pntpbnd  27524  pntibnd  27529  nosupno  27640  noinfno  27655  noetasuplem4  27673  noetalem1  27678  madebday  27843  cofcutr  27866  negsprop  27975  mulscom  28076  absmuls  28180  zs12ge0  28391  remulscl  28402  tgjustr  28450  tglowdim1i  28477  tgbtwndiff  28482  tgifscgr  28484  iscgrglt  28490  tgcgrxfr  28494  lnext  28543  tgbtwnconn1lem3  28550  tgbtwnconn1  28551  legval  28560  legov  28561  legov2  28562  legtrd  28565  legtri3  28566  legso  28575  hlcgrex  28592  hlcgreu  28594  tglnne  28604  tglndim0  28605  tglineeltr  28607  tglinethru  28612  tglnne0  28616  tglnpt2  28617  colline  28625  tglowdim2l  28626  tglowdim2ln  28627  mirreu3  28630  miriso  28646  midexlem  28668  isperp  28688  perpcom  28689  perpneq  28690  isperp2  28691  footexALT  28694  footex  28697  colperpexlem3  28708  opphllem  28711  midex  28713  oppne3  28719  opptgdim2  28721  opphllem2  28724  opphllem3  28725  opphllem5  28727  opphllem6  28728  opphl  28730  outpasch  28731  lnopp2hpgb  28739  colopp  28745  lmieu  28760  trgcopy  28780  trgcopyeu  28782  iscgra1  28786  cgrane1  28788  cgrane2  28789  cgrane3  28790  cgrahl1  28792  cgrahl2  28793  cgracgr  28794  cgraswap  28796  cgracom  28798  cgratr  28799  flatcgra  28800  cgrabtwn  28802  cgrahl  28803  dfcgra2  28806  sacgr  28807  acopyeu  28810  inaghl  28821  cgrg3col4  28829  f1otrg  28847  f1otrge  28848  axsegcon  28903  axeuclidlem  28938  upgr1eopALT  29093  usgr1eop  29226  pthdepisspth  29711  wpthswwlks2on  29937  clwwlkf1  30024  clwwlknscsh  30037  2pthfrgr  30259  n4cyclfrgr  30266  frgrwopreglem5  30296  frgrwopreglem5ALT  30297  friendshipgt3  30373  smcnlem  30672  0lno  30765  ubthlem1  30845  ubthlem3  30847  chocunii  31276  occl  31279  5oalem1  31629  3oalem2  31638  nmopub2tALT  31884  nmfnleub2  31901  lnconi  32008  kbass5  32095  mdslmd1lem1  32300  mdslmd1lem2  32301  cdj1i  32408  opreu2reuALT  32451  disjabrex  32557  disjabrexf  32558  2ndresdju  32626  acunirnmpt  32636  acunirnmpt2  32637  acunirnmpt2f  32638  aciunf1lem  32639  fnpreimac  32648  fgreu  32649  suppovss  32657  xrge0infss  32738  xrofsup  32745  elq2  32789  fsumiunle  32807  sgnsub  32815  2exple2exp  32823  s3f1  32923  ccatf1  32925  ccatws1f1o  32927  swrdf1  32932  ressprs  32942  dfmgc2  32972  mgcf1o  32979  xrge0addgt0  32993  mndlrinvb  33001  mndlactf1  33002  mndlactfo  33003  mndractf1  33004  mndractfo  33005  mndlactf1o  33006  gsumfs2d  33030  gsumwun  33040  gsumwrd2dccatlem  33041  psgnfzto1stlem  33064  fzto1st1  33066  cycpmco2  33097  cycpmrn  33107  cyc3genpm  33116  cycpmconjs  33120  cyc3conja  33121  conjga  33134  fxpsubrg  33138  submarchi  33150  isarchi3  33151  archiabllem1  33157  archiabllem2a  33158  isarchiofld  33163  elrgspnlem1  33204  elrgspnlem2  33205  elrgspnlem4  33207  elrgspnsubrunlem2  33210  erler  33227  rlocaddval  33230  rlocmulval  33231  rloccring  33232  rloc1r  33234  subrdom  33246  isdrng4  33256  fracfld  33269  imaslmod  33313  dvdsruasso  33345  unitprodclb  33349  nsgqusf1olem2  33374  lmhmqusker  33377  intlidl  33380  rhmquskerlem  33385  elrspunidl  33388  elrspunsn  33389  rhmimaidl  33392  prmidl2  33401  isprmidlc  33407  rhmpreimaprmidl  33411  qsidomlem2  33413  ssdifidllem  33416  ssdifidlprm  33418  mxidlprm  33430  ssmxidl  33434  opprqusplusg  33449  opprqusmulr  33451  qsdrngilem  33454  qsdrngi  33455  rsprprmprmidl  33482  rsprprmprmidlb  33483  rprmirred  33491  rprmirredb  33492  rprmdvdspow  33493  rprmdvdsprod  33494  1arithidom  33497  1arithufdlem2  33505  1arithufdlem3  33506  1arithufdlem4  33507  dfufd2lem  33509  dfufd2  33510  zringfrac  33514  ply1dg3rt0irred  33541  r1plmhm  33565  r1pquslmic  33566  mplvrpmga  33570  exsslsb  33604  lindsunlem  33632  lindsun  33633  dimkerim  33635  fedgmullem1  33637  fedgmul  33639  dimlssid  33640  evls1fldgencl  33678  fldextrspunlsplem  33681  extdgfialg  33702  minplyirred  33719  fldext2chn  33736  constrmon  33752  constrconj  33753  constrfin  33754  constrelextdg2  33755  constrextdg2lem  33756  constrextdg2  33757  constrext2chnlem  33758  constrfiss  33759  cos9thpiminplylem2  33791  mdetpmtr1  33831  txomap  33842  qtophaus  33844  cmpcref  33858  zarclsun  33878  zarclssn  33881  zarcmplem  33889  pstmxmet  33905  sqsscirc1  33916  ordtrest2NEWlem  33930  ordtconnlem1  33932  pnfneige0  33959  lmxrge0  33960  lmdvg  33961  qqhval2  33990  esumcst  34071  esumrnmpt2  34076  esumfsup  34078  esumcvg  34094  esum2d  34101  esumiun  34102  sigaclfu2  34129  insiga  34145  ldsysgenld  34168  ldgenpisyslem1  34171  fiunelros  34182  measinb  34229  imambfm  34270  oms0  34305  omssubadd  34308  carsgclctunlem3  34328  eulerpartlemgvv  34384  dstrvprob  34480  signstfvneq0  34580  actfunsnrndisj  34613  reprinfz1  34630  breprexp  34641  afsval  34679  derangenlem  35203  sconnpi1  35271  cvmsss2  35306  cvmopnlem  35310  cvmlift3lem7  35357  msrval  35570  ifscgr  36077  cgrxfr  36088  btwnconn1lem13  36132  outsideofeu  36164  neibastop2lem  36393  weiunso  36499  irrdifflemf  37358  irrdiff  37359  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem14  37673  poimirlem22  37681  poimirlem29  37688  broucube  37693  heicant  37694  mblfinlem1  37696  itg2addnclem  37710  ftc1cnnc  37731  ftc1anclem7  37738  sstotbnd2  37813  equivtotbnd  37817  isbnd3  37823  ssbnd  37827  totbndbnd  37828  cntotbnd  37835  heibor1lem  37848  rrncmslem  37871  lssats  39050  lsat0cv  39071  lkrlss  39133  lfl1dim  39159  lfl1dim2N  39160  lkrpssN  39201  hlhgt2  39427  3dim2  39506  2dim  39508  lplncvrlvol  39654  paddasslem11  39868  pmapjat1  39891  2polssN  39953  pclfinclN  39988  pexmidlem8N  40015  lhpexle1lem  40045  4atex  40114  ltrnid  40173  trlator0  40209  cdlemg2cex  40629  tendodi1  40822  tendodi2  40823  diblss  41208  dihopelvalcpre  41286  dihatexv  41376  mapdval4N  41670  fldhmf1  42122  mndmolinv  42127  primrootscoprmpow  42131  posbezout  42132  primrootscoprbij2  42135  primrootspoweq0  42138  aks6d1c2p2  42151  hashscontpow  42154  aks6d1c2lem4  42159  aks6d1c2  42162  aks6d1c5  42171  sticksstones8  42185  sticksstones12  42190  sticksstones22  42200  aks6d1c6lem3  42204  aks6d1c6isolem1  42206  unitscyglem3  42229  aks5  42236  sn-subeu  42459  sn-0tie0  42483  fiabv  42568  frlmsnic  42572  fsuppind  42622  prjspersym  42639  dffltz  42666  nna4b4nsq  42692  mzpindd  42778  mzpsubst  42780  mzpcompact2lem  42783  eldioph2b  42795  irrapxlem3  42856  irrapxlem5  42858  pellex  42867  pell1234qrdich  42893  pell14qrexpcl  42899  congabseq  43006  jm2.26a  43032  jm2.26lem3  43033  rmydioph  43046  lnrfg  43151  hbt  43162  cantnftermord  43352  cantnfresb  43356  cantnf2  43357  oawordex2  43358  omabs2  43364  tfsconcatfv  43373  tfsconcatrev  43380  ofoaass  43392  nadd2rabtr  43416  nadd1suc  43424  naddgeoa  43426  rfovcnvf1od  44036  clsk3nimkb  44072  ntrneiiso  44123  ntrneikb  44126  ntrneixb  44127  ntrneik3  44128  ntrneix3  44129  ntrneik13  44130  ntrneix13  44131  4an4132  44531  iunconnlem2  44966  modelaxrep  45013  fnchoice  45065  cncmpmax  45068  ssinc  45123  ssdec  45124  disjf1  45219  supxrge  45376  suplesup  45377  infxr  45404  infleinf  45409  unb2ltle  45452  rexabslelem  45455  uzub  45468  supminfxr  45501  climrec  45642  climsuse  45647  islptre  45658  addlimc  45685  0ellimcdiv  45686  limsuppnfdlem  45738  limsupub  45741  limsuppnflem  45747  limsupubuz  45750  climinf3  45753  limsupmnflem  45757  climxrre  45787  liminfreuzlem  45839  liminflimsupclim  45844  xlimliminflimsup  45899  icccncfext  45924  cncfiooicclem1  45930  fperdvper  45956  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvmptfprodlem  45981  dvmptfprod  45982  dvnprodlem2  45984  stoweidlem7  46044  stoweidlem34  46071  stoweidlem52  46089  stoweidlem60  46097  wallispilem3  46104  fourierdlem34  46178  fourierdlem38  46182  fourierdlem39  46183  fourierdlem48  46191  fourierdlem50  46193  fourierdlem51  46194  fourierdlem73  46216  fourierdlem76  46219  fourierdlem77  46220  fourierdlem80  46223  fourierdlem87  46230  fourierdlem103  46246  fourierdlem104  46247  etransclem32  46303  etransclem33  46304  sge0f1o  46419  sge0pr  46431  sge0isum  46464  iundjiun  46497  meaiininclem  46523  pimdecfgtioo  46754  pimincfltioo  46755  preimageiingt  46757  preimaleiinlt  46758  smflimlem2  46809  smflimlem4  46811  smfmullem3  46830  smflimmpt  46847  smfinflem  46854  smfpimne2  46877  fsupdm  46879  finfdm  46883  cfsetsnfsetfo  47090  funressnbrafv2  47274  imasetpreimafvbijlemf1  47434  bgoldbtbndlem2  47836  bgoldbtbndlem3  47837  bgoldbtbnd  47839  isuspgrim  47926  stgrusgra  47989  isubgr3stgrlem6  48001  2zlidl  48270  lindslinindsimp2  48494  snlindsntor  48502  lincresunit2  48509  islindeps2  48514  imaf1co  49186  imasubc3  49187  fucofvalg  49349  fuco21  49367  precofvalALT  49399  lanfval  49644  ranfval  49645