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  6329  fsnex  7275  soisoi  7320  f1o2ndf1  8119  fimaproj  8132  fprlem2  8298  tz7.49  8457  omabs  8661  cofon1  8682  naddssim  8695  omxpenlem  9085  fopwdom  9092  findcard3  9288  findcard3OLD  9289  frfi  9291  finsschain  9369  marypha1lem  9443  wemappo  9561  wdomtr  9587  cantnfp1  9693  ttrcltr  9728  harcard  9990  numacn  10061  infunsdom1  10224  sornom  10289  ssfin4  10322  fin1a2lem11  10422  fin1a2lem13  10424  fpwwe2lem12  10654  pwfseq  10676  mulcmpblnr  11083  00id  11408  addrid  11413  cnegex  11414  negeu  11470  add20  11747  ltmul12a  12095  lediv12a  12133  cru  12230  qextltlem  13216  xleadd1a  13267  xmullem  13278  xlemul1a  13302  ixxss12  13380  ioodisj  13497  fvf1tp  13804  fsuppmapnn0fz  14012  seqf1o  14059  mulexpz  14118  leexp1a  14191  faclbnd  14306  swrdswrdlem  14720  abs3lem  15355  rexico  15370  cau3lem  15371  rlim3  15512  ello12  15530  lo1bdd2  15538  elo12  15541  rlimconst  15558  isercoll  15682  climcau  15685  climbdd  15686  summolem2  15730  fsumconst  15804  o1fsum  15827  incexclem  15850  fprodconst  15992  bitsfzo  16452  dvdsmulgcd  16573  pc2dvds  16897  pcz  16899  pcadd  16907  pcfac  16917  vdwmc2  16997  vdwlem2  17000  vdwlem10  17008  vdw  17012  ramcl  17047  sbcie3s  17179  firest  17444  prdsval  17467  mreexd  17652  mreexexlemd  17654  iscat  17682  cidfval  17686  iscatd2  17691  catcocl  17695  catass  17696  catpropd  17719  cidpropd  17720  moni  17747  monpropd  17748  issubc  17846  subccocl  17856  funcco  17882  funcpropd  17913  fullpropd  17933  nati  17969  natpropd  17990  fucpropd  17991  xpcpropd  18218  curfuncf  18248  curf2ndf  18257  yonffthlem  18292  acsfiindd  18561  mgmhmeql  18692  sgrppropd  18707  mndpropd  18735  mhmeql  18802  smndex1mgm  18883  isgrpinv  18974  dfgrp3lem  19019  mhmmnd  19045  cycsubm  19183  cycsubmcom  19185  conjnmzb  19234  ghmqusnsg  19263  ghmquskerlem3  19267  ghmqusker  19268  gass  19282  symgextf  19396  dfod2  19543  gexdvds  19563  sylow3lem2  19607  efgredlem  19726  efgredeu  19731  ghmcmn  19810  oddvdssubg  19834  dprdfcntz  19996  pgpfaclem3  20064  isrng  20112  issrg  20146  isring  20195  dvdsrmul1  20327  issubdrg  20738  islmhm2  20994  lmhmeql  21011  lssacsex  21103  rhmpreimaidl  21236  rhmqusnsg  21244  isphl  21586  uvcf1  21750  lindfmm  21785  sraassab  21826  issubassa2  21850  opsrval  22002  psdmul  22102  scmatmats  22447  smatvscl  22460  mdetunilem7  22554  gsummatr01lem4  22594  m2cpmfo  22692  pmatcollpw3fi1lem1  22722  pm2mpf1lem  22730  pm2mpf1  22735  mp2pm2mplem4  22745  pm2mpghm  22752  chfacfscmulfsupp  22795  chfacfpmmulfsupp  22799  cctop  22942  neiptoptop  23067  neiptopreu  23069  tgrest  23095  ordtrest2lem  23139  cnss1  23212  cncnp  23216  isnrm3  23295  uncmp  23339  cmpfi  23344  iunconn  23364  1stcrest  23389  subislly  23417  islly2  23420  cldllycmp  23431  lly1stc  23432  llycmpkgen2  23486  kgencn  23492  xkoccn  23555  ptcnplem  23557  pthaus  23574  txhaus  23583  txkgen  23588  xkohaus  23589  xkococnlem  23595  txconn  23625  regr1lem2  23676  kqreglem1  23677  reghmph  23729  nrmhmph  23730  trfil2  23823  ufileu  23855  flimopn  23911  flimcf  23918  fclscf  23961  ufilcmp  23968  cnpfcf  23977  cnextfun  24000  tgpmulg  24029  symgtgp  24042  tgpt0  24055  qustgplem  24057  ustex2sym  24153  ustex3sym  24154  trust  24166  restutop  24174  restutopopn  24175  ustuqtop4  24181  utop3cls  24188  utopreg  24189  cstucnd  24220  ucncn  24221  trcfilu  24230  neipcfilu  24232  ismet2  24270  metequiv2  24447  metcnp  24478  metcnp2  24479  metcnpi3  24483  txmetcnp  24484  metustto  24490  metustsym  24492  metust  24495  cfilucfil  24496  metuel2  24502  psmetutop  24504  restmetu  24507  metucn  24508  ngptgp  24573  tngngp  24591  nmoleub  24668  icccmp  24763  reconnlem2  24765  reconn  24766  xmetdcn2  24775  metdseq0  24792  metdscn  24794  elcncf2  24832  cncfmet  24851  cnheibor  24903  nmoleub2lem2  25065  nmoleub3  25068  cvsi  25079  iscfil2  25216  iscfil3  25223  cfilfcls  25224  equivcfil  25249  caubl  25258  bcthlem5  25278  pmltpc  25401  ovollb2  25440  ovoliunnul  25458  ovolicc2lem4  25471  volsup  25507  ioorf  25524  dyadss  25545  dyaddisjlem  25546  mbfposr  25603  cncombf  25609  mbflimsup  25617  i1fmulclem  25653  mbfi1fseqlem4  25669  iblss2  25757  ellimc2  25828  ellimc3  25830  dvnadd  25881  dvmptfsum  25929  dvferm1  25939  dvferm2  25941  fta1g  26125  plyeq0lem  26165  plydivex  26255  fta1  26266  aalioulem2  26291  aalioulem3  26292  ulmuni  26351  ulmbdd  26357  ulmdvlem3  26361  mtest  26363  abelthlem8  26399  efopn  26617  cxpmul2z  26650  cxpcn3lem  26707  jensen  26949  lgambdd  26997  lgamucov  26998  isppw2  27075  mersenne  27188  dchrelbas3  27199  dchrptlem1  27225  dchrpt  27228  lgsval2lem  27268  lgsdchrval  27315  lgsquad3  27348  2sqb  27393  2sqmo  27398  pntrsumbnd2  27528  pntpbnd  27549  pntibnd  27554  nosupno  27665  noinfno  27680  noetasuplem4  27698  noetalem1  27703  madebday  27855  cofcutr  27875  negsprop  27984  mulscom  28082  absmuls  28185  remulscl  28351  tgjustr  28399  tglowdim1i  28426  tgbtwndiff  28431  tgifscgr  28433  iscgrglt  28439  tgcgrxfr  28443  lnext  28492  tgbtwnconn1lem3  28499  tgbtwnconn1  28500  legval  28509  legov  28510  legov2  28511  legtrd  28514  legtri3  28515  legso  28524  hlcgrex  28541  hlcgreu  28543  tglnne  28553  tglndim0  28554  tglineeltr  28556  tglinethru  28561  tglnne0  28565  tglnpt2  28566  colline  28574  tglowdim2l  28575  tglowdim2ln  28576  mirreu3  28579  miriso  28595  midexlem  28617  isperp  28637  perpcom  28638  perpneq  28639  isperp2  28640  footexALT  28643  footex  28646  colperpexlem3  28657  opphllem  28660  midex  28662  oppne3  28668  opptgdim2  28670  opphllem2  28673  opphllem3  28674  opphllem5  28676  opphllem6  28677  opphl  28679  outpasch  28680  lnopp2hpgb  28688  colopp  28694  lmieu  28709  trgcopy  28729  trgcopyeu  28731  iscgra1  28735  cgrane1  28737  cgrane2  28738  cgrane3  28739  cgrahl1  28741  cgrahl2  28742  cgracgr  28743  cgraswap  28745  cgracom  28747  cgratr  28748  flatcgra  28749  cgrabtwn  28751  cgrahl  28752  dfcgra2  28755  sacgr  28756  acopyeu  28759  inaghl  28770  cgrg3col4  28778  f1otrg  28796  f1otrge  28797  axsegcon  28852  axeuclidlem  28887  upgr1eopALT  29042  usgr1eop  29175  pthdepisspth  29663  wpthswwlks2on  29889  clwwlkf1  29976  clwwlknscsh  29989  2pthfrgr  30211  n4cyclfrgr  30218  frgrwopreglem5  30248  frgrwopreglem5ALT  30249  friendshipgt3  30325  smcnlem  30624  0lno  30717  ubthlem1  30797  ubthlem3  30799  chocunii  31228  occl  31231  5oalem1  31581  3oalem2  31590  nmopub2tALT  31836  nmfnleub2  31853  lnconi  31960  kbass5  32047  mdslmd1lem1  32252  mdslmd1lem2  32253  cdj1i  32360  opreu2reuALT  32404  disjabrex  32509  disjabrexf  32510  2ndresdju  32573  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1lem  32586  fnpreimac  32595  fgreu  32596  suppovss  32604  xrge0infss  32683  xrofsup  32690  elq2  32736  fsumiunle  32754  sgnsub  32762  2exple2exp  32770  s3f1  32868  ccatf1  32870  ccatws1f1o  32873  swrdf1  32878  ressprs  32890  dfmgc2  32922  mgcf1o  32929  chnind  32937  chnso  32940  xrge0addgt0  32958  mndlrinvb  32966  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  mndlactf1o  32971  gsumfs2d  32995  gsumwun  33005  gsumwrd2dccatlem  33006  gsumle  33038  psgnfzto1stlem  33057  fzto1st1  33059  cycpmco2  33090  cycpmrn  33100  cyc3genpm  33109  cycpmconjs  33113  cyc3conja  33114  submarchi  33130  isarchi3  33131  archiabllem1  33137  archiabllem2a  33138  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem2  33189  erler  33206  rlocaddval  33209  rlocmulval  33210  rloccring  33211  rloc1r  33213  subrdom  33225  isdrng4  33235  fracfld  33248  suborng  33283  isarchiofld  33285  imaslmod  33314  dvdsruasso  33346  unitprodclb  33350  nsgqusf1olem2  33375  lmhmqusker  33378  intlidl  33381  rhmquskerlem  33386  elrspunidl  33389  elrspunsn  33390  rhmimaidl  33393  prmidl2  33402  isprmidlc  33408  rhmpreimaprmidl  33412  qsidomlem2  33414  ssdifidllem  33417  ssdifidlprm  33419  mxidlprm  33431  ssmxidl  33435  opprqusplusg  33450  opprqusmulr  33452  qsdrngilem  33455  qsdrngi  33456  rsprprmprmidl  33483  rsprprmprmidlb  33484  rprmirred  33492  rprmirredb  33493  rprmdvdspow  33494  rprmdvdsprod  33495  1arithidom  33498  1arithufdlem2  33506  1arithufdlem3  33507  1arithufdlem4  33508  dfufd2lem  33510  dfufd2  33511  zringfrac  33515  ply1dg3rt0irred  33541  r1plmhm  33565  r1pquslmic  33566  exsslsb  33582  lindsunlem  33610  lindsun  33611  dimkerim  33613  fedgmullem1  33615  fedgmul  33617  dimlssid  33618  evls1fldgencl  33657  fldextrspunlsplem  33660  minplyirred  33691  fldext2chn  33708  constrmon  33724  constrconj  33725  constrfin  33726  constrelextdg2  33727  constrextdg2lem  33728  constrextdg2  33729  constrext2chnlem  33730  constrfiss  33731  cos9thpiminplylem2  33763  mdetpmtr1  33800  txomap  33811  qtophaus  33813  cmpcref  33827  zarclsun  33847  zarclssn  33850  zarcmplem  33858  pstmxmet  33874  sqsscirc1  33885  ordtrest2NEWlem  33899  ordtconnlem1  33901  pnfneige0  33928  lmxrge0  33929  lmdvg  33930  qqhval2  33959  esumcst  34040  esumrnmpt2  34045  esumfsup  34047  esumcvg  34063  esum2d  34070  esumiun  34071  sigaclfu2  34098  insiga  34114  ldsysgenld  34137  ldgenpisyslem1  34140  fiunelros  34151  measinb  34198  imambfm  34240  oms0  34275  omssubadd  34278  carsgclctunlem3  34298  eulerpartlemgvv  34354  dstrvprob  34450  signstfvneq0  34550  actfunsnrndisj  34583  reprinfz1  34600  breprexp  34611  afsval  34649  derangenlem  35139  sconnpi1  35207  cvmsss2  35242  cvmopnlem  35246  cvmlift3lem7  35293  msrval  35506  ifscgr  36008  cgrxfr  36019  btwnconn1lem13  36063  outsideofeu  36095  neibastop2lem  36324  weiunso  36430  irrdifflemf  37289  irrdiff  37290  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem14  37604  poimirlem22  37612  poimirlem29  37619  broucube  37624  heicant  37625  mblfinlem1  37627  itg2addnclem  37641  ftc1cnnc  37662  ftc1anclem7  37669  sstotbnd2  37744  equivtotbnd  37748  isbnd3  37754  ssbnd  37758  totbndbnd  37759  cntotbnd  37766  heibor1lem  37779  rrncmslem  37802  lssats  38976  lsat0cv  38997  lkrlss  39059  lfl1dim  39085  lfl1dim2N  39086  lkrpssN  39127  hlhgt2  39354  3dim2  39433  2dim  39435  lplncvrlvol  39581  paddasslem11  39795  pmapjat1  39818  2polssN  39880  pclfinclN  39915  pexmidlem8N  39942  lhpexle1lem  39972  4atex  40041  ltrnid  40100  trlator0  40136  cdlemg2cex  40556  tendodi1  40749  tendodi2  40750  diblss  41135  dihopelvalcpre  41213  dihatexv  41303  mapdval4N  41597  fldhmf1  42049  mndmolinv  42054  primrootscoprmpow  42058  posbezout  42059  primrootscoprbij2  42062  primrootspoweq0  42065  aks6d1c2p2  42078  hashscontpow  42081  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c5  42098  sticksstones8  42112  sticksstones12  42117  sticksstones22  42127  aks6d1c6lem3  42131  aks6d1c6isolem1  42133  unitscyglem3  42156  aks5  42163  metakunt1  42164  metakunt2  42165  sn-subeu  42416  sn-0tie0  42429  fiabv  42506  frlmsnic  42510  fsuppind  42560  prjspersym  42577  dffltz  42604  nna4b4nsq  42630  mzpindd  42716  mzpsubst  42718  mzpcompact2lem  42721  eldioph2b  42733  irrapxlem3  42794  irrapxlem5  42796  pellex  42805  pell1234qrdich  42831  pell14qrexpcl  42837  congabseq  42945  jm2.26a  42971  jm2.26lem3  42972  rmydioph  42985  lnrfg  43090  hbt  43101  cantnftermord  43291  cantnfresb  43295  cantnf2  43296  oawordex2  43297  omabs2  43303  tfsconcatfv  43312  tfsconcatrev  43319  ofoaass  43331  nadd2rabtr  43355  nadd1suc  43363  naddgeoa  43365  rfovcnvf1od  43975  clsk3nimkb  44011  ntrneiiso  44062  ntrneikb  44065  ntrneixb  44066  ntrneik3  44067  ntrneix3  44068  ntrneik13  44069  ntrneix13  44070  4an4132  44472  iunconnlem2  44907  modelaxrep  44954  fnchoice  45001  cncmpmax  45004  ssinc  45059  ssdec  45060  disjf1  45155  supxrge  45313  suplesup  45314  infxr  45342  infleinf  45347  unb2ltle  45390  rexabslelem  45393  uzub  45406  supminfxr  45439  climrec  45580  climsuse  45585  islptre  45596  addlimc  45625  0ellimcdiv  45626  limsuppnfdlem  45678  limsupub  45681  limsuppnflem  45687  limsupubuz  45690  climinf3  45693  limsupmnflem  45697  climxrre  45727  liminfreuzlem  45779  liminflimsupclim  45784  xlimliminflimsup  45839  icccncfext  45864  cncfiooicclem1  45870  fperdvper  45896  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvmptfprodlem  45921  dvmptfprod  45922  dvnprodlem2  45924  stoweidlem7  45984  stoweidlem34  46011  stoweidlem52  46029  stoweidlem60  46037  wallispilem3  46044  fourierdlem34  46118  fourierdlem38  46122  fourierdlem39  46123  fourierdlem48  46131  fourierdlem50  46133  fourierdlem51  46134  fourierdlem73  46156  fourierdlem76  46159  fourierdlem77  46160  fourierdlem80  46163  fourierdlem87  46170  fourierdlem103  46186  fourierdlem104  46187  etransclem32  46243  etransclem33  46244  sge0f1o  46359  sge0pr  46371  sge0isum  46404  iundjiun  46437  meaiininclem  46463  pimdecfgtioo  46694  pimincfltioo  46695  preimageiingt  46697  preimaleiinlt  46698  smflimlem2  46749  smflimlem4  46751  smfmullem3  46770  smflimmpt  46787  smfinflem  46794  smfpimne2  46817  fsupdm  46819  finfdm  46823  cfsetsnfsetfo  47037  funressnbrafv2  47221  imasetpreimafvbijlemf1  47366  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbnd  47771  isuspgrim  47857  stgrusgra  47919  isubgr3stgrlem6  47931  2zlidl  48163  lindslinindsimp2  48387  snlindsntor  48395  lincresunit2  48402  islindeps2  48407  imaf1co  49043  imasubc3  49044  fucofvalg  49177  fuco21  49195  precofvalALT  49227  lanfval  49438  ranfval  49439