Theorem simpllr 776

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 732	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  6306  fsnex  7239  soisoi  7284  f1o2ndf1  8074  fimaproj  8087  fprlem2  8253  tz7.49  8386  omabs  8589  cofon1  8610  naddssim  8623  omxpenlem  9018  fopwdom  9025  findcard3  9195  frfi  9197  finsschain  9271  marypha1lem  9348  wemappo  9466  wdomtr  9492  cantnfp1  9602  ttrcltr  9637  harcard  9902  numacn  9971  infunsdom1  10134  sornom  10199  ssfin4  10232  fin1a2lem11  10332  fin1a2lem13  10334  fpwwe2lem12  10565  pwfseq  10587  mulcmpblnr  10994  00id  11320  addrid  11325  cnegex  11326  negeu  11382  add20  11661  ltmul12a  12009  lediv12a  12047  cru  12149  qextltlem  13129  xleadd1a  13180  xmullem  13191  xlemul1a  13215  ixxss12  13293  ioodisj  13410  fvf1tp  13721  fsuppmapnn0fz  13931  seqf1o  13978  mulexpz  14037  leexp1a  14110  faclbnd  14225  swrdswrdlem  14639  abs3lem  15274  rexico  15289  cau3lem  15290  rlim3  15433  ello12  15451  lo1bdd2  15459  elo12  15462  rlimconst  15479  isercoll  15603  climcau  15606  climbdd  15607  summolem2  15651  fsumconst  15725  o1fsum  15748  incexclem  15771  fprodconst  15913  bitsfzo  16374  dvdsmulgcd  16495  pc2dvds  16819  pcz  16821  pcadd  16829  pcfac  16839  vdwmc2  16919  vdwlem2  16922  vdwlem10  16930  vdw  16934  ramcl  16969  sbcie3s  17101  firest  17364  prdsval  17387  mreexd  17577  mreexexlemd  17579  iscat  17607  cidfval  17611  iscatd2  17616  catcocl  17620  catass  17621  catpropd  17644  cidpropd  17645  moni  17672  monpropd  17673  issubc  17771  subccocl  17781  funcco  17807  funcpropd  17838  fullpropd  17858  nati  17894  natpropd  17915  fucpropd  17916  xpcpropd  18143  curfuncf  18173  curf2ndf  18182  yonffthlem  18217  acsfiindd  18488  chnind  18556  chnso  18559  mgmhmeql  18653  sgrppropd  18668  mndpropd  18696  mhmeql  18763  smndex1mgm  18844  isgrpinv  18935  dfgrp3lem  18980  mhmmnd  19006  cycsubm  19143  cycsubmcom  19145  conjnmzb  19194  ghmqusnsg  19223  ghmquskerlem3  19227  ghmqusker  19228  gass  19242  symgextf  19358  dfod2  19505  gexdvds  19525  sylow3lem2  19569  efgredlem  19688  efgredeu  19693  ghmcmn  19772  oddvdssubg  19796  dprdfcntz  19958  pgpfaclem3  20026  gsumle  20086  isrng  20101  issrg  20135  isring  20184  dvdsrmul1  20317  issubdrg  20725  suborng  20821  islmhm2  21002  lmhmeql  21019  lssacsex  21111  rhmpreimaidl  21244  rhmqusnsg  21252  isphl  21595  uvcf1  21759  lindfmm  21794  sraassab  21835  issubassa2  21860  opsrval  22013  psdmul  22121  scmatmats  22467  smatvscl  22480  mdetunilem7  22574  gsummatr01lem4  22614  m2cpmfo  22712  pmatcollpw3fi1lem1  22742  pm2mpf1lem  22750  pm2mpf1  22755  mp2pm2mplem4  22765  pm2mpghm  22772  chfacfscmulfsupp  22815  chfacfpmmulfsupp  22819  cctop  22962  neiptoptop  23087  neiptopreu  23089  tgrest  23115  ordtrest2lem  23159  cnss1  23232  cncnp  23236  isnrm3  23315  uncmp  23359  cmpfi  23364  iunconn  23384  1stcrest  23409  subislly  23437  islly2  23440  cldllycmp  23451  lly1stc  23452  llycmpkgen2  23506  kgencn  23512  xkoccn  23575  ptcnplem  23577  pthaus  23594  txhaus  23603  txkgen  23608  xkohaus  23609  xkococnlem  23615  txconn  23645  regr1lem2  23696  kqreglem1  23697  reghmph  23749  nrmhmph  23750  trfil2  23843  ufileu  23875  flimopn  23931  flimcf  23938  fclscf  23981  ufilcmp  23988  cnpfcf  23997  cnextfun  24020  tgpmulg  24049  symgtgp  24062  tgpt0  24075  qustgplem  24077  ustex2sym  24173  ustex3sym  24174  trust  24185  restutop  24193  restutopopn  24194  ustuqtop4  24200  utop3cls  24207  utopreg  24208  cstucnd  24239  ucncn  24240  trcfilu  24249  neipcfilu  24251  ismet2  24289  metequiv2  24466  metcnp  24497  metcnp2  24498  metcnpi3  24502  txmetcnp  24503  metustto  24509  metustsym  24511  metust  24514  cfilucfil  24515  metuel2  24521  psmetutop  24523  restmetu  24526  metucn  24527  ngptgp  24592  tngngp  24610  nmoleub  24687  icccmp  24782  reconnlem2  24784  reconn  24785  xmetdcn2  24794  metdseq0  24811  metdscn  24813  elcncf2  24851  cncfmet  24870  cnheibor  24922  nmoleub2lem2  25084  nmoleub3  25087  cvsi  25098  iscfil2  25234  iscfil3  25241  cfilfcls  25242  equivcfil  25267  caubl  25276  bcthlem5  25296  pmltpc  25419  ovollb2  25458  ovoliunnul  25476  ovolicc2lem4  25489  volsup  25525  ioorf  25542  dyadss  25563  dyaddisjlem  25564  mbfposr  25621  cncombf  25627  mbflimsup  25635  i1fmulclem  25671  mbfi1fseqlem4  25687  iblss2  25775  ellimc2  25846  ellimc3  25848  dvnadd  25899  dvmptfsum  25947  dvferm1  25957  dvferm2  25959  fta1g  26143  plyeq0lem  26183  plydivex  26273  fta1  26284  aalioulem2  26309  aalioulem3  26310  ulmuni  26369  ulmbdd  26375  ulmdvlem3  26379  mtest  26381  abelthlem8  26417  efopn  26635  cxpmul2z  26668  cxpcn3lem  26725  jensen  26967  lgambdd  27015  lgamucov  27016  isppw2  27093  mersenne  27206  dchrelbas3  27217  dchrptlem1  27243  dchrpt  27246  lgsval2lem  27286  lgsdchrval  27333  lgsquad3  27366  2sqb  27411  2sqmo  27416  pntrsumbnd2  27546  pntpbnd  27567  pntibnd  27572  nosupno  27683  noinfno  27698  noetasuplem4  27716  noetalem1  27721  madebday  27908  cofcutr  27932  negsprop  28043  mulscom  28147  absmuls  28252  addonbday  28287  bdayfinbndlem1  28475  z12sge0  28491  remulscl  28510  tgjustr  28558  tglowdim1i  28585  tgbtwndiff  28590  tgifscgr  28592  iscgrglt  28598  tgcgrxfr  28602  lnext  28651  tgbtwnconn1lem3  28658  tgbtwnconn1  28659  legval  28668  legov  28669  legov2  28670  legtrd  28673  legtri3  28674  legso  28683  hlcgrex  28700  hlcgreu  28702  tglnne  28712  tglndim0  28713  tglineeltr  28715  tglinethru  28720  tglnne0  28724  tglnpt2  28725  colline  28733  tglowdim2l  28734  tglowdim2ln  28735  mirreu3  28738  miriso  28754  midexlem  28776  isperp  28796  perpcom  28797  perpneq  28798  isperp2  28799  footexALT  28802  footex  28805  colperpexlem3  28816  opphllem  28819  midex  28821  oppne3  28827  opptgdim2  28829  opphllem2  28832  opphllem3  28833  opphllem5  28835  opphllem6  28836  opphl  28838  outpasch  28839  lnopp2hpgb  28847  colopp  28853  lmieu  28868  trgcopy  28888  trgcopyeu  28890  iscgra1  28894  cgrane1  28896  cgrane2  28897  cgrane3  28898  cgrahl1  28900  cgrahl2  28901  cgracgr  28902  cgraswap  28904  cgracom  28906  cgratr  28907  flatcgra  28908  cgrabtwn  28910  cgrahl  28911  dfcgra2  28914  sacgr  28915  acopyeu  28918  inaghl  28929  cgrg3col4  28937  f1otrg  28955  f1otrge  28956  axsegcon  29012  axeuclidlem  29047  upgr1eopALT  29202  usgr1eop  29335  pthdepisspth  29820  wpthswwlks2on  30049  clwwlkf1  30136  clwwlknscsh  30149  2pthfrgr  30371  n4cyclfrgr  30378  frgrwopreglem5  30408  frgrwopreglem5ALT  30409  friendshipgt3  30485  smcnlem  30784  0lno  30877  ubthlem1  30957  ubthlem3  30959  chocunii  31388  occl  31391  5oalem1  31741  3oalem2  31750  nmopub2tALT  31996  nmfnleub2  32013  lnconi  32120  kbass5  32207  mdslmd1lem1  32412  mdslmd1lem2  32413  cdj1i  32520  opreu2reuALT  32562  disjabrex  32668  disjabrexf  32669  2ndresdju  32738  acunirnmpt  32748  acunirnmpt2  32749  acunirnmpt2f  32750  aciunf1lem  32751  fnpreimac  32759  fgreu  32760  suppovss  32770  xrge0infss  32850  xrofsup  32857  elq2  32902  fsumiunle  32920  sgnsub  32928  2exple2exp  32936  s3f1  33039  ccatf1  33041  ccatws1f1o  33043  swrdf1  33048  ressprs  33058  dfmgc2  33088  mgcf1o  33095  xrge0addgt0  33109  mndlrinvb  33117  mndlactf1  33118  mndlactfo  33119  mndractf1  33120  mndractfo  33121  mndlactf1o  33122  gsumfs2d  33154  suppgsumssiun  33165  gsumwun  33169  gsumwrd2dccatlem  33170  psgnfzto1stlem  33193  fzto1st1  33195  cycpmco2  33226  cycpmrn  33236  cyc3genpm  33245  cycpmconjs  33249  cyc3conja  33250  conjga  33263  fxpsubrg  33267  submarchi  33279  isarchi3  33280  archiabllem1  33286  archiabllem2a  33287  isarchiofld  33292  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrunlem2  33341  erler  33358  rlocaddval  33361  rlocmulval  33362  rloccring  33363  rloc1r  33365  subrdom  33378  isdrng4  33388  fracfld  33401  imaslmod  33445  dvdsruasso  33477  unitprodclb  33481  nsgqusf1olem2  33506  lmhmqusker  33509  intlidl  33512  rhmquskerlem  33517  elrspunidl  33520  elrspunsn  33521  rhmimaidl  33524  prmidl2  33533  isprmidlc  33539  rhmpreimaprmidl  33543  qsidomlem2  33545  ssdifidllem  33548  ssdifidlprm  33550  mxidlprm  33562  ssmxidl  33566  opprqusplusg  33581  opprqusmulr  33583  qsdrngilem  33586  qsdrngi  33587  rsprprmprmidl  33614  rsprprmprmidlb  33615  rprmirred  33623  rprmirredb  33624  rprmdvdspow  33625  rprmdvdsprod  33626  1arithidom  33629  1arithufdlem2  33637  1arithufdlem3  33638  1arithufdlem4  33639  dfufd2lem  33641  dfufd2  33642  zringfrac  33646  deg1prod  33675  ply1dg3rt0irred  33676  r1plmhm  33702  r1pquslmic  33703  extvfvcl  33712  mplmulmvr  33715  mplvrpmga  33721  psrgsum  33724  psrmonprod  33728  esplyfval3  33748  esplyfval1  33749  esplyfvaln  33750  esplyind  33751  exsslsb  33773  lindsunlem  33801  lindsun  33802  dimkerim  33804  fedgmullem1  33806  fedgmul  33808  dimlssid  33809  evls1fldgencl  33847  fldextrspunlsplem  33850  extdgfialg  33871  minplyirred  33888  fldext2chn  33905  constrmon  33921  constrconj  33922  constrfin  33923  constrelextdg2  33924  constrextdg2lem  33925  constrextdg2  33926  constrext2chnlem  33927  constrfiss  33928  cos9thpiminplylem2  33960  mdetpmtr1  34000  txomap  34011  qtophaus  34013  cmpcref  34027  zarclsun  34047  zarclssn  34050  zarcmplem  34058  pstmxmet  34074  sqsscirc1  34085  ordtrest2NEWlem  34099  ordtconnlem1  34101  pnfneige0  34128  lmxrge0  34129  lmdvg  34130  qqhval2  34159  esumcst  34240  esumrnmpt2  34245  esumfsup  34247  esumcvg  34263  esum2d  34270  esumiun  34271  sigaclfu2  34298  insiga  34314  ldsysgenld  34337  ldgenpisyslem1  34340  fiunelros  34351  measinb  34398  imambfm  34439  oms0  34474  omssubadd  34477  carsgclctunlem3  34497  eulerpartlemgvv  34553  dstrvprob  34649  signstfvneq0  34749  actfunsnrndisj  34782  reprinfz1  34799  breprexp  34810  afsval  34848  derangenlem  35384  sconnpi1  35452  cvmsss2  35487  cvmopnlem  35491  cvmlift3lem7  35538  msrval  35751  ifscgr  36257  cgrxfr  36268  btwnconn1lem13  36312  outsideofeu  36344  neibastop2lem  36573  weiunso  36679  irrdifflemf  37577  irrdiff  37578  matunitlindflem1  37864  matunitlindflem2  37865  poimirlem14  37882  poimirlem22  37890  poimirlem29  37897  broucube  37902  heicant  37903  mblfinlem1  37905  itg2addnclem  37919  ftc1cnnc  37940  ftc1anclem7  37947  sstotbnd2  38022  equivtotbnd  38026  isbnd3  38032  ssbnd  38036  totbndbnd  38037  cntotbnd  38044  heibor1lem  38057  rrncmslem  38080  lssats  39385  lsat0cv  39406  lkrlss  39468  lfl1dim  39494  lfl1dim2N  39495  lkrpssN  39536  hlhgt2  39762  3dim2  39841  2dim  39843  lplncvrlvol  39989  paddasslem11  40203  pmapjat1  40226  2polssN  40288  pclfinclN  40323  pexmidlem8N  40350  lhpexle1lem  40380  4atex  40449  ltrnid  40508  trlator0  40544  cdlemg2cex  40964  tendodi1  41157  tendodi2  41158  diblss  41543  dihopelvalcpre  41621  dihatexv  41711  mapdval4N  42005  fldhmf1  42457  mndmolinv  42462  primrootscoprmpow  42466  posbezout  42467  primrootscoprbij2  42470  primrootspoweq0  42473  aks6d1c2p2  42486  hashscontpow  42489  aks6d1c2lem4  42494  aks6d1c2  42497  aks6d1c5  42506  sticksstones8  42520  sticksstones12  42525  sticksstones22  42535  aks6d1c6lem3  42539  aks6d1c6isolem1  42541  unitscyglem3  42564  aks5  42571  sn-subeu  42794  sn-0tie0  42818  fiabv  42903  frlmsnic  42907  fsuppind  42945  prjspersym  42962  dffltz  42989  nna4b4nsq  43015  mzpindd  43100  mzpsubst  43102  mzpcompact2lem  43105  eldioph2b  43117  irrapxlem3  43178  irrapxlem5  43180  pellex  43189  pell1234qrdich  43215  pell14qrexpcl  43221  congabseq  43328  jm2.26a  43354  jm2.26lem3  43355  rmydioph  43368  lnrfg  43473  hbt  43484  cantnftermord  43674  cantnfresb  43678  cantnf2  43679  oawordex2  43680  omabs2  43686  tfsconcatfv  43695  tfsconcatrev  43702  ofoaass  43714  nadd2rabtr  43738  nadd1suc  43746  naddgeoa  43748  rfovcnvf1od  44357  clsk3nimkb  44393  ntrneiiso  44444  ntrneikb  44447  ntrneixb  44448  ntrneik3  44449  ntrneix3  44450  ntrneik13  44451  ntrneix13  44452  4an4132  44852  iunconnlem2  45287  modelaxrep  45334  fnchoice  45386  cncmpmax  45389  ssinc  45443  ssdec  45444  disjf1  45539  supxrge  45694  suplesup  45695  infxr  45722  infleinf  45727  unb2ltle  45770  rexabslelem  45773  uzub  45786  supminfxr  45819  climrec  45960  climsuse  45965  islptre  45976  addlimc  46003  0ellimcdiv  46004  limsuppnfdlem  46056  limsupub  46059  limsuppnflem  46065  limsupubuz  46068  climinf3  46071  limsupmnflem  46075  climxrre  46105  liminfreuzlem  46157  liminflimsupclim  46162  xlimliminflimsup  46217  icccncfext  46242  cncfiooicclem1  46248  fperdvper  46274  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvmptfprodlem  46299  dvmptfprod  46300  dvnprodlem2  46302  stoweidlem7  46362  stoweidlem34  46389  stoweidlem52  46407  stoweidlem60  46415  wallispilem3  46422  fourierdlem34  46496  fourierdlem38  46500  fourierdlem39  46501  fourierdlem48  46509  fourierdlem50  46511  fourierdlem51  46512  fourierdlem73  46534  fourierdlem76  46537  fourierdlem77  46538  fourierdlem80  46541  fourierdlem87  46548  fourierdlem103  46564  fourierdlem104  46565  etransclem32  46621  etransclem33  46622  sge0f1o  46737  sge0pr  46749  sge0isum  46782  iundjiun  46815  meaiininclem  46841  pimdecfgtioo  47072  pimincfltioo  47073  preimageiingt  47075  preimaleiinlt  47076  smflimlem2  47127  smflimlem4  47129  smfmullem3  47148  smflimmpt  47165  smfinflem  47172  smfpimne2  47195  fsupdm  47197  finfdm  47201  cfsetsnfsetfo  47417  funressnbrafv2  47601  imasetpreimafvbijlemf1  47761  bgoldbtbndlem2  48163  bgoldbtbndlem3  48164  bgoldbtbnd  48166  isuspgrim  48253  stgrusgra  48316  isubgr3stgrlem6  48328  2zlidl  48597  lindslinindsimp2  48820  snlindsntor  48828  lincresunit2  48835  islindeps2  48840  imaf1co  49511  imasubc3  49512  fucofvalg  49674  fuco21  49692  precofvalALT  49724  lanfval  49969  ranfval  49970