Theorem simpllr 785

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 741	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  frpomin  6323  fsnex  7263  soisoi  7308  f1o2ndf1  8096  fimaproj  8110  fprlem2  8277  tz7.49  8411  omabs  8616  cofon1  8637  naddssim  8651  omxpenlem  9046  fopwdom  9053  findcard3  9223  frfi  9225  finsschain  9299  marypha1lem  9376  wemappo  9494  wdomtr  9520  cantnfp1  9633  ttrcltr  9668  harcard  9933  numacn  10002  infunsdom1  10165  sornom  10231  ssfin4  10264  fin1a2lem11  10364  fin1a2lem13  10366  fpwwe2lem12  10597  pwfseq  10619  mulcmpblnr  11026  00id  11355  addrid  11360  cnegex  11361  negeu  11417  add20  11696  ltmul12a  12044  lediv12a  12082  cru  12184  qextltlem  13202  xleadd1a  13253  xmullem  13264  xlemul1a  13288  ixxss12  13366  ioodisj  13483  fvf1tp  13796  fsuppmapnn0fz  14006  seqf1o  14053  mulexpz  14112  leexp1a  14185  faclbnd  14300  swrdswrdlem  14714  abs3lem  15349  rexico  15364  cau3lem  15365  rlim3  15508  ello12  15526  lo1bdd2  15534  elo12  15537  rlimconst  15554  isercoll  15678  climcau  15681  climbdd  15682  summolem2  15726  fsumconst  15800  o1fsum  15824  incexclem  15849  fprodconst  15991  bitsfzo  16452  dvdsmulgcd  16573  pc2dvds  16898  pcz  16900  pcadd  16908  pcfac  16918  vdwmc2  16998  vdwlem2  17001  vdwlem10  17009  vdw  17013  ramcl  17048  sbcie3s  17181  firest  17444  prdsval  17467  mreexd  17657  mreexexlemd  17659  iscat  17687  cidfval  17691  iscatd2  17696  catcocl  17700  catass  17701  catpropd  17724  cidpropd  17725  moni  17752  monpropd  17753  issubc  17851  subccocl  17861  funcco  17887  funcpropd  17918  fullpropd  17938  nati  17974  natpropd  17995  fucpropd  17996  xpcpropd  18223  curfuncf  18253  curf2ndf  18262  yonffthlem  18297  acsfiindd  18568  chnind  18636  chnso  18639  mgmhmeql  18733  sgrppropd  18748  mndpropd  18776  mhmeql  18843  smndex1mgm  18927  isgrpinv  19018  dfgrp3lem  19063  mhmmnd  19089  cycsubm  19226  cycsubmcom  19228  conjnmzb  19276  ghmqusnsg  19305  ghmquskerlem3  19309  ghmqusker  19310  gass  19324  symgextf  19440  dfod2  19587  gexdvds  19607  sylow3lem2  19651  efgredlem  19770  efgredeu  19775  ghmcmn  19854  oddvdssubg  19878  dprdfcntz  20040  pgpfaclem3  20108  gsumle  20168  isrng  20183  issrg  20217  isring  20266  dvdsrmul1  20397  issubdrg  20809  suborng  20905  islmhm2  21085  lmhmeql  21102  lssacsex  21194  rhmpreimaidl  21327  rhmqusnsg  21335  isphl  21660  uvcf1  21824  lindfmm  21859  sraassab  21900  issubassa2  21924  opsrval  22079  psdmul  22211  scmatmats  22551  smatvscl  22564  mdetunilem7  22658  gsummatr01lem4  22698  m2cpmfo  22796  pmatcollpw3fi1lem1  22826  pm2mpf1lem  22834  pm2mpf1  22839  mp2pm2mplem4  22849  pm2mpghm  22856  chfacfscmulfsupp  22899  chfacfpmmulfsupp  22903  cctop  23046  neiptoptop  23171  neiptopreu  23173  tgrest  23199  ordtrest2lem  23243  cnss1  23316  cncnp  23320  isnrm3  23399  uncmp  23443  cmpfi  23448  iunconn  23468  1stcrest  23493  subislly  23521  islly2  23524  cldllycmp  23535  lly1stc  23536  llycmpkgen2  23590  kgencn  23596  xkoccn  23659  ptcnplem  23661  pthaus  23678  txhaus  23687  txkgen  23692  xkohaus  23693  xkococnlem  23699  txconn  23729  regr1lem2  23780  kqreglem1  23781  reghmph  23833  nrmhmph  23834  trfil2  23927  ufileu  23959  flimopn  24015  flimcf  24022  fclscf  24065  ufilcmp  24072  cnpfcf  24081  cnextfun  24104  tgpmulg  24133  symgtgp  24146  tgpt0  24159  qustgplem  24161  ustex2sym  24257  ustex3sym  24258  trust  24269  restutop  24277  restutopopn  24278  ustuqtop4  24284  utop3cls  24291  utopreg  24292  cstucnd  24323  ucncn  24324  trcfilu  24333  neipcfilu  24335  ismet2  24373  metequiv2  24550  metcnp  24581  metcnp2  24582  metcnpi3  24586  txmetcnp  24587  metustto  24593  metustsym  24595  metust  24598  cfilucfil  24599  metuel2  24605  psmetutop  24607  restmetu  24610  metucn  24611  ngptgp  24676  tngngp  24694  nmoleub  24771  icccmp  24866  reconnlem2  24868  reconn  24869  xmetdcn2  24878  metdseq0  24895  metdscn  24897  elcncf2  24932  cncfmet  24951  cnheibor  24997  nmoleub2lem2  25158  nmoleub3  25161  cvsi  25172  iscfil2  25308  iscfil3  25315  cfilfcls  25316  equivcfil  25341  caubl  25350  bcthlem5  25370  pmltpc  25492  ovollb2  25531  ovoliunnul  25549  ovolicc2lem4  25562  volsup  25598  ioorf  25615  dyadss  25636  dyaddisjlem  25637  mbfposr  25694  cncombf  25700  mbflimsup  25708  i1fmulclem  25744  mbfi1fseqlem4  25760  iblss2  25848  ellimc2  25919  ellimc3  25921  dvnadd  25971  dvmptfsum  26017  dvferm1  26027  dvferm2  26029  fta1g  26210  plyeq0lem  26250  plydivex  26338  fta1  26349  aalioulem2  26374  aalioulem3  26375  ulmuni  26432  ulmbdd  26438  ulmdvlem3  26442  mtest  26444  abelthlem8  26479  efopn  26700  cxpmul2z  26733  cxpcn3lem  26789  jensen  27030  lgambdd  27078  lgamucov  27079  isppw2  27156  mersenne  27268  dchrelbas3  27279  dchrptlem1  27305  dchrpt  27308  lgsval2lem  27348  lgsdchrval  27395  lgsquad3  27428  2sqb  27473  2sqmo  27478  pntrsumbnd2  27608  pntpbnd  27629  pntibnd  27634  nosupno  27744  noinfno  27759  noetasuplem4  27777  noetalem1  27782  madebday  27970  cofcutr  27994  negsprop  28105  mulscom  28209  absmuls  28314  addonbday  28349  bdayfinbndlem1  28537  z12sge0  28553  remulscl  28572  tgjustr  28620  tglowdim1i  28647  tgbtwndiff  28652  tgifscgr  28654  iscgrglt  28660  tgcgrxfr  28664  lnext  28713  tgbtwnconn1lem3  28720  tgbtwnconn1  28721  legval  28730  legov  28731  legov2  28732  legtrd  28735  legtri3  28736  legso  28745  hlcgrex  28762  hlcgreu  28764  tglnne  28774  tglndim0  28775  tglineeltr  28777  tglinethru  28782  tglnne0  28786  tglnpt2  28787  colline  28795  tglowdim2l  28796  tglowdim2ln  28797  mirreu3  28800  miriso  28816  midexlem  28838  isperp  28858  perpcom  28859  perpneq  28860  isperp2  28861  footexALT  28864  footex  28867  colperpexlem3  28878  opphllem  28881  midex  28883  oppne3  28889  opptgdim2  28891  opphllem2  28894  opphllem3  28895  opphllem5  28897  opphllem6  28898  opphl  28900  outpasch  28901  lnopp2hpgb  28909  colopp  28915  lmieu  28930  trgcopy  28950  trgcopyeu  28952  iscgra1  28956  cgrane1  28958  cgrane2  28959  cgrane3  28960  cgrahl1  28962  cgrahl2  28963  cgracgr  28964  cgraswap  28966  cgracom  28968  cgratr  28969  flatcgra  28970  cgrabtwn  28972  cgrahl  28973  dfcgra2  28976  sacgr  28977  acopyeu  28980  inaghl  28991  cgrg3col4  28999  f1otrg  29017  f1otrge  29018  axsegcon  29074  axeuclidlem  29109  upgr1eopALT  29264  usgr1eop  29397  pthdepisspth  29881  wpthswwlks2on  30110  clwwlkf1  30197  clwwlknscsh  30210  2pthfrgr  30432  n4cyclfrgr  30439  frgrwopreglem5  30469  frgrwopreglem5ALT  30470  friendshipgt3  30546  smcnlem  30846  0lno  30939  ubthlem1  31019  ubthlem3  31021  chocunii  31450  occl  31453  5oalem1  31803  3oalem2  31812  nmopub2tALT  32058  nmfnleub2  32075  lnconi  32182  kbass5  32269  mdslmd1lem1  32474  mdslmd1lem2  32475  cdj1i  32582  opreu2reuALT  32624  disjabrex  32731  disjabrexf  32732  2ndresdju  32801  acunirnmpt  32811  acunirnmpt2  32812  acunirnmpt2f  32813  aciunf1lem  32814  fnpreimac  32822  fgreu  32823  suppovss  32833  xrge0infss  32912  xrofsup  32919  elq2  32964  fsumiunle  32981  sgnsub  32989  2exple2exp  32997  s3f1  33086  ccatf1  33088  ccatws1f1o  33090  swrdf1  33095  ressprs  33105  dfmgc2  33135  mgcf1o  33142  xrge0addgt0  33156  mndlrinvb  33164  mndlactf1  33165  mndlactfo  33166  mndractf1  33167  mndractfo  33168  mndlactf1o  33169  gsumfs2d  33202  suppgsumssiun  33213  gsumwun  33217  gsumwrd2dccatlem  33218  psgnfzto1stlem  33241  fzto1st1  33243  cycpmco2  33274  cycpmrn  33284  cyc3genpm  33293  cycpmconjs  33297  cyc3conja  33298  conjga  33311  fxpsubrg  33315  submarchi  33327  isarchi3  33328  archiabllem1  33334  archiabllem2a  33335  isarchiofld  33340  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem4  33387  elrgspnsubrunlem2  33390  erler  33407  rlocaddval  33411  rlocmulval  33412  rloccring  33413  rloc1r  33415  rlocisunit  33418  subrdom  33430  ricdomn1  33434  isdrng4  33443  fracfld  33456  imaslmod  33500  dvdsruasso  33532  unitprodclb  33536  nsgqusf1olem2  33561  lmhmqusker  33564  intlidl  33567  rhmquskerlem  33572  elrspunidl  33575  elrspunsn  33576  rhmimaidl  33579  prmidl2  33588  isprmidlc  33594  rhmpreimaprmidl  33599  qsidomlem2  33601  ssdifidllem  33604  ssdifidlprm  33606  mxidlprm  33619  ssmxidl  33623  opprqusplusg  33638  opprqusmulr  33640  qsdrngilem  33643  qsdrngi  33644  drnglring  33649  dflring2  33650  dflringlem2  33652  rsprprmprmidl  33679  rsprprmprmidlb  33680  rprmirred  33688  rprmirredb  33689  rprmdvdspow  33690  rprmdvdsprod  33691  1arithidom  33694  1arithufdlem2  33702  1arithufdlem3  33703  1arithufdlem4  33704  dfufd2lem  33706  dfufd2  33707  zringfrac  33711  deg1prod  33740  ply1dg3rt0irred  33741  r1plmhm  33767  r1pquslmic  33768  0mplrim  33772  mplidomlem  33785  extvfvcl  33794  mplmulmvr  33797  mplvrpmga  33803  psrgsum  33806  psrmonprod  33810  esplyfval3  33830  esplyfval1  33831  esplyfvaln  33832  esplyind  33833  exsslsb  33855  lindsunlem  33882  lindsun  33883  dimkerim  33885  fedgmullem1  33887  fedgmul  33889  dimlssid  33890  evls1fldgencl  33928  fldextrspunlsplem  33931  extdgfialg  33952  minplyirred  33969  fldext2chn  33986  constrmon  34002  constrconj  34003  constrfin  34004  constrelextdg2  34005  constrextdg2lem  34006  constrextdg2  34007  constrext2chnlem  34008  constrfiss  34009  cos9thpiminplylem2  34041  mdetpmtr1  34081  txomap  34092  qtophaus  34094  cmpcref  34108  zarclsun  34128  zarclssn  34131  zarcmplem  34139  pstmxmet  34155  sqsscirc1  34166  ordtrest2NEWlem  34180  ordtconnlem1  34182  pnfneige0  34209  lmxrge0  34210  lmdvg  34211  qqhval2  34240  esumcst  34321  esumrnmpt2  34326  esumfsup  34328  esumcvg  34344  esum2d  34351  esumiun  34352  sigaclfu2  34379  insiga  34395  ldsysgenld  34418  ldgenpisyslem1  34421  fiunelros  34432  measinb  34479  imambfm  34520  oms0  34555  omssubadd  34558  carsgclctunlem3  34578  eulerpartlemgvv  34634  dstrvprob  34730  signstfvneq0  34830  actfunsnrndisj  34863  reprinfz1  34880  breprexp  34891  afsval  34932  derangenlem  35485  sconnpi1  35553  cvmsss2  35588  cvmopnlem  35592  cvmlift3lem7  35639  msrval  35852  ifscgr  36358  cgrxfr  36369  btwnconn1lem13  36413  outsideofeu  36445  nmulcom  36508  neibastop2lem  36684  weiunso  36790  irrdifflemf  37781  irrdiff  37782  matunitlindflem1  38079  matunitlindflem2  38080  poimirlem14  38097  poimirlem22  38105  poimirlem29  38112  broucube  38117  heicant  38118  mblfinlem1  38120  itg2addnclem  38134  ftc1cnnc  38155  ftc1anclem7  38162  sstotbnd2  38237  equivtotbnd  38241  isbnd3  38247  ssbnd  38251  totbndbnd  38252  cntotbnd  38259  heibor1lem  38272  rrncmslem  38295  lssats  39600  lsat0cv  39621  lkrlss  39683  lfl1dim  39709  lfl1dim2N  39710  lkrpssN  39751  hlhgt2  39977  3dim2  40056  2dim  40058  lplncvrlvol  40204  paddasslem11  40418  pmapjat1  40441  2polssN  40503  pclfinclN  40538  pexmidlem8N  40565  lhpexle1lem  40595  4atex  40664  ltrnid  40723  trlator0  40759  cdlemg2cex  41179  tendodi1  41372  tendodi2  41373  diblss  41758  dihopelvalcpre  41836  dihatexv  41926  mapdval4N  42220  fldhmf1  42671  mndmolinv  42676  primrootscoprmpow  42680  posbezout  42681  primrootscoprbij2  42684  primrootspoweq0  42687  aks6d1c2p2  42700  hashscontpow  42703  aks6d1c2lem4  42708  aks6d1c2  42711  aks6d1c5  42720  sticksstones8  42734  sticksstones12  42739  sticksstones22  42749  aks6d1c6lem3  42753  aks6d1c6isolem1  42755  unitscyglem3  42778  aks5  42785  sn-subeu  43000  sn-0tie0  43037  fiabv  43118  frlmsnic  43122  fsuppind  43136  prjspersym  43153  dffltz  43180  nna4b4nsq  43206  mzpindd  43291  mzpsubst  43293  mzpcompact2lem  43296  eldioph2b  43308  irrapxlem3  43365  irrapxlem5  43367  pellex  43376  pell1234qrdich  43402  pell14qrexpcl  43408  congabseq  43515  jm2.26a  43541  jm2.26lem3  43542  rmydioph  43555  lnrfg  43660  hbt  43671  cantnftermord  43861  cantnfresb  43865  cantnf2  43866  oawordex2  43867  omabs2  43873  tfsconcatfv  43882  tfsconcatrev  43889  ofoaass  43901  nadd2rabtr  43925  nadd1suc  43933  naddgeoa  43935  rfovcnvf1od  44544  clsk3nimkb  44580  ntrneiiso  44631  ntrneikb  44634  ntrneixb  44635  ntrneik3  44636  ntrneix3  44637  ntrneik13  44638  ntrneix13  44639  4an4132  45039  iunconnlem2  45474  modelaxrep  45521  fnchoice  45573  cncmpmax  45576  ssinc  45629  ssdec  45630  disjf1  45725  supxrge  45878  suplesup  45879  infxr  45906  infleinf  45911  unb2ltle  45953  rexabslelem  45956  uzub  45969  supminfxr  46002  climrec  46143  climsuse  46148  islptre  46159  addlimc  46186  0ellimcdiv  46187  limsuppnfdlem  46239  limsupub  46242  limsuppnflem  46248  limsupubuz  46251  climinf3  46254  limsupmnflem  46258  climxrre  46288  liminfreuzlem  46340  liminflimsupclim  46345  xlimliminflimsup  46400  icccncfext  46425  cncfiooicclem1  46431  fperdvper  46457  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvmptfprodlem  46482  dvmptfprod  46483  dvnprodlem2  46485  stoweidlem7  46545  stoweidlem34  46572  stoweidlem52  46590  stoweidlem60  46598  wallispilem3  46605  fourierdlem34  46679  fourierdlem38  46683  fourierdlem39  46684  fourierdlem48  46692  fourierdlem50  46694  fourierdlem51  46695  fourierdlem73  46717  fourierdlem76  46720  fourierdlem77  46721  fourierdlem80  46724  fourierdlem87  46731  fourierdlem103  46747  fourierdlem104  46748  etransclem32  46804  etransclem33  46805  sge0f1o  46920  sge0pr  46932  sge0isum  46965  iundjiun  46998  meaiininclem  47024  hoicvr  47086  pimdecfgtioo  47255  pimincfltioo  47256  preimageiingt  47258  preimaleiinlt  47259  smflimlem2  47310  smflimlem4  47312  smfmullem3  47331  smflimmpt  47348  smfinflem  47355  smfpimne2  47378  fsupdm  47380  finfdm  47384  cfsetsnfsetfo  47618  funressnbrafv2  47802  imasetpreimafvbijlemf1  47974  bgoldbtbndlem2  48392  bgoldbtbndlem3  48393  bgoldbtbnd  48395  isuspgrim  48482  stgrusgra  48545  isubgr3stgrlem6  48557  2zlidl  48826  lindslinindsimp2  49049  snlindsntor  49057  lincresunit2  49064  islindeps2  49069  imaf1co  49740  imasubc3  49741  fucofvalg  49903  fuco21  49921  precofvalALT  49953  lanfval  50198  ranfval  50199