Theorem simpllr 788

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 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad3antlr 744	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  frpomin  6348  fsnex  7292  soisoi  7337  f1o2ndf1  8126  fimaproj  8140  fprlem2  8307  tz7.49  8441  omabs  8646  cofon1  8667  naddssim  8681  omxpenlem  9076  fopwdom  9083  findcard3  9253  frfi  9255  finsschain  9326  marypha1lem  9403  wemappo  9521  wdomtr  9547  cantnfp1  9660  ttrcltr  9695  harcard  9983  numacn  10052  infunsdom1  10214  sornom  10279  ssfin4  10312  fin1a2lem11  10412  fin1a2lem13  10414  fpwwe2lem12  10645  pwfseq  10667  mulcmpblnr  11074  00id  11403  addrid  11408  cnegex  11409  negeu  11465  add20  11744  ltmul12a  12089  lediv12a  12126  cru  12228  qextltlem  13246  xleadd1a  13297  xmullem  13308  xlemul1a  13332  ixxss12  13410  ioodisj  13527  fvf1tp  13842  fsuppmapnn0fz  14052  seqf1o  14099  mulexpz  14158  leexp1a  14231  faclbnd  14346  ccatf1  14648  swrdf1  14711  swrdswrdlem  14765  sgnsub  15169  abs3lem  15416  rexico  15431  cau3lem  15432  rlim3  15575  ello12  15593  lo1bdd2  15601  elo12  15604  rlimconst  15621  isercoll  15745  climcau  15748  climbdd  15749  summolem2  15793  fsumconst  15867  o1fsum  15891  incexclem  15916  fprodconst  16058  bitsfzo  16518  dvdsmulgcd  16639  pc2dvds  16964  pcz  16966  pcadd  16974  pcfac  16984  vdwmc2  17064  vdwlem2  17067  vdwlem10  17075  vdw  17079  ramcl  17114  sbcie3s  17247  firest  17510  prdsval  17533  mreexd  17723  mreexexlemd  17725  iscat  17753  cidfval  17757  iscatd2  17762  catcocl  17766  catass  17767  catpropd  17790  cidpropd  17791  moni  17818  monpropd  17819  issubc  17917  subccocl  17927  funcco  17953  funcpropd  17984  fullpropd  18004  nati  18040  natpropd  18061  fucpropd  18062  xpcpropd  18289  curfuncf  18319  curf2ndf  18328  yonffthlem  18363  acsfiindd  18634  chnind  18702  chnso  18705  mgmhmeql  18803  sgrppropd  18818  mndpropd  18846  mhmeql  18916  smndex1mgm  19000  isgrpinv  19091  dfgrp3lem  19135  mhmmnd  19161  cycsubm  19304  cycsubmcom  19306  conjnmzb  19354  ghmqusnsg  19383  ghmquskerlem3  19387  ghmqusker  19388  gass  19402  symgextf  19518  dfod2  19665  gexdvds  19685  sylow3lem2  19729  efgredlem  19848  efgredeu  19853  ghmcmn  19932  oddvdssubg  19956  dprdfcntz  20118  pgpfaclem3  20186  gsumle  20246  isrng  20263  issrg  20301  isring  20350  dvdsrmul1  20484  isdrng4  20876  issubdrg  20920  suborng  21016  islmhm2  21196  lmhmeql  21213  lssacsex  21305  rhmpreimaidl  21453  rhmqusnsg  21462  prmidl2  21503  isprmidlc  21509  rhmpreimaprmidl  21516  qsidomlem2  21518  ssdifidllem  21521  ssdifidlprm  21523  isphl  21815  uvcf1  21979  lindfmm  22014  sraassab  22055  issubassa2  22079  opsrval  22234  psdmul  22366  scmatmats  22705  smatvscl  22718  mdetunilem7  22812  gsummatr01lem4  22852  m2cpmfo  22950  pmatcollpw3fi1lem1  22980  pm2mpf1lem  22988  pm2mpf1  22993  mp2pm2mplem4  23003  pm2mpghm  23010  chfacfscmulfsupp  23053  chfacfpmmulfsupp  23057  cctop  23200  neiptoptop  23325  neiptopreu  23327  tgrest  23353  ordtrest2lem  23397  cnss1  23470  cncnp  23474  isnrm3  23553  uncmp  23597  cmpfi  23602  iunconn  23622  1stcrest  23647  subislly  23675  islly2  23678  cldllycmp  23689  lly1stc  23690  llycmpkgen2  23744  kgencn  23750  xkoccn  23813  ptcnplem  23815  pthaus  23832  txhaus  23841  txkgen  23846  xkohaus  23847  xkococnlem  23853  txconn  23883  regr1lem2  23934  kqreglem1  23935  reghmph  23987  nrmhmph  23988  trfil2  24081  ufileu  24113  flimopn  24169  flimcf  24176  fclscf  24219  ufilcmp  24226  cnpfcf  24235  cnextfun  24258  tgpmulg  24287  symgtgp  24300  tgpt0  24313  qustgplem  24315  ustex2sym  24411  ustex3sym  24412  trust  24423  restutop  24431  restutopopn  24432  ustuqtop4  24438  utop3cls  24445  utopreg  24446  cstucnd  24477  ucncn  24478  trcfilu  24487  neipcfilu  24489  ismet2  24527  metequiv2  24704  metcnp  24735  metcnp2  24736  metcnpi3  24740  txmetcnp  24741  metustto  24747  metustsym  24749  metust  24752  cfilucfil  24753  metuel2  24759  psmetutop  24761  restmetu  24764  metucn  24765  ngptgp  24830  tngngp  24848  nmoleub  24925  icccmp  25020  reconnlem2  25022  reconn  25023  xmetdcn2  25032  metdseq0  25049  metdscn  25051  elcncf2  25086  cncfmet  25105  cnheibor  25151  nmoleub2lem2  25312  nmoleub3  25315  cvsi  25326  iscfil2  25462  iscfil3  25469  cfilfcls  25470  equivcfil  25495  caubl  25504  bcthlem5  25524  pmltpc  25646  ovollb2  25685  ovoliunnul  25703  ovolicc2lem4  25716  volsup  25752  ioorf  25769  dyadss  25790  dyaddisjlem  25791  mbfposr  25848  cncombf  25854  mbflimsup  25862  i1fmulclem  25898  mbfi1fseqlem4  25914  iblss2  26002  ellimc2  26073  ellimc3  26075  dvnadd  26125  dvmptfsum  26171  dvferm1  26181  dvferm2  26183  fta1g  26364  plyeq0lem  26404  plydivex  26495  fta1  26506  aalioulem2  26533  aalioulem3  26534  ulmuni  26592  ulmbdd  26598  ulmdvlem3  26602  mtest  26604  abelthlem8  26639  efopn  26860  cxpmul2z  26893  cxpcn3lem  26949  jensen  27190  lgambdd  27238  lgamucov  27239  isppw2  27316  mersenne  27428  dchrelbas3  27439  dchrptlem1  27465  dchrpt  27468  lgsval2lem  27508  lgsdchrval  27555  lgsquad3  27588  2sqb  27633  2sqmo  27638  pntrsumbnd2  27768  pntpbnd  27789  pntibnd  27794  nosupno  27904  noinfno  27919  noetasuplem4  27937  noetalem1  27942  madebday  28130  cofcutr  28154  negsprop  28265  mulscom  28369  absmuls  28474  addonbday  28509  bdayfinbndlem1  28697  z12sge0  28713  remulscl  28732  tgjustr  28780  tglowdim1i  28807  tgbtwndiff  28812  tgifscgr  28814  iscgrglt  28820  tgcgrxfr  28824  lnext  28873  tgbtwnconn1lem3  28880  tgbtwnconn1  28881  legval  28890  legov  28891  legov2  28892  legtrd  28895  legtri3  28896  legso  28905  hlcgrex  28925  hlcgreu  28927  tglnne  28938  tglndim0  28939  tglineeltr  28941  tglinethru  28946  tglinesseq  28950  tglnne0  28951  colline  28960  tglowdim2l  28961  tglowdim2ln  28962  tglnpt2  28963  tglnpt3  28964  tglnpt4  28965  mirreu3  28968  miriso  28984  midexlem  29006  isperp  29029  perpcom  29030  perpneq  29031  isperp2  29032  footexALT  29035  footex  29038  colperpexlem3  29050  opphllem  29053  midex  29055  oppne3  29061  opptgdim2  29063  opphllem2  29066  opphllem3  29067  opphllem5  29069  opphllem6  29070  opphl  29072  outpasch  29074  lnopp2hpgb  29082  colopp  29088  plngrnssp  29098  lnincplng  29103  plngrotlem1  29106  plngrotlem3  29108  lnssplng  29111  plng3p  29116  lmieu  29130  trgcopy  29152  trgcopyeu  29154  iscgra1  29158  cgrane1  29160  cgrane2  29161  cgrane3  29162  cgrahl1  29164  cgrahl2  29165  cgracgr  29166  cgraswap  29168  cgracom  29170  cgratr  29171  flatcgra  29172  cgrabtwn  29174  cgrahl  29175  dfcgra2  29178  sacgr  29179  acopyeu  29182  ragcgra  29183  cgrarag  29184  ragsupplcgra  29185  inaghl  29199  cgrg3col4  29207  prlnghpg  29233  dfprlng2  29234  dfprlng3  29235  perpprlng  29237  prlngex  29238  prlngmolem1  29239  prlngmolem2  29240  prlngmo2  29243  prlngplngtr  29246  quadcgrprlng  29253  f1otrg  29257  f1otrge  29258  axsegcon  29314  axeuclidlem  29349  upgr1eopALT  29504  usgr1eop  29637  pthdepisspth  30121  wpthswwlks2on  30350  clwwlkf1  30437  clwwlknscsh  30450  2pthfrgr  30672  n4cyclfrgr  30679  frgrwopreglem5  30709  frgrwopreglem5ALT  30710  friendshipgt3  30786  smcnlem  31086  0lno  31179  ubthlem1  31259  ubthlem3  31261  chocunii  31690  occl  31693  5oalem1  32043  3oalem2  32052  nmopub2tALT  32298  nmfnleub2  32315  lnconi  32422  kbass5  32509  mdslmd1lem1  32714  mdslmd1lem2  32715  cdj1i  32822  opreu2reuALT  32860  disjabrex  32964  disjabrexf  32965  2ndresdju  33031  acunirnmpt  33041  acunirnmpt2  33042  acunirnmpt2f  33043  aciunf1lem  33044  fnpreimac  33052  fgreu  33053  suppovss  33063  xrge0infss  33142  xrofsup  33149  elq2  33193  fsumiunle  33210  2exple2exp  33215  s3f1  33301  ccatws1f1o  33304  ressprs  33317  dfmgc2  33347  mgcf1o  33354  xrge0addgt0  33368  mndlrinvb  33376  mndlactf1  33377  mndlactfo  33378  mndractf1  33379  mndractfo  33380  mndlactf1o  33381  gsumfs2d  33412  suppgsumssiun  33423  gsumwun  33427  gsumwrd2dccatlem  33428  psgnfzto1stlem  33451  fzto1st1  33453  cycpmco2  33484  cycpmrn  33494  cyc3genpm  33503  cycpmconjs  33507  cyc3conja  33508  conjga  33521  fxpsubrg  33525  submarchi  33537  isarchi3  33538  archiabllem1  33544  archiabllem2a  33545  isarchiofld  33550  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem4  33596  elrgspnsubrunlem2  33599  erler  33616  rlocaddval  33620  rlocmulval  33621  rloccring  33622  rloc1r  33624  rlocisunit  33627  subrdom  33636  ricdomn1  33640  fracfld  33660  imaslmod  33704  dvdsruasso  33729  unitprodclb  33733  nsgqusf1olem2  33754  lmhmqusker  33757  intlidl  33759  rhmquskerlem  33764  elrspunidl  33767  elrspunsn  33768  rhmimaidl  33771  mxidlprm  33784  ssmxidl  33788  opprqusplusg  33802  opprqusmulr  33804  qsdrngilem  33807  qsdrngi  33808  drnglring  33813  dflring2  33814  dflringlem2  33816  rsprprmprmidl  33843  rsprprmprmidlb  33844  rprmirred  33852  rprmirredb  33853  rprmdvdspow  33854  rprmdvdsprod  33855  1arithidom  33858  1arithufdlem2  33866  1arithufdlem3  33867  1arithufdlem4  33868  dfufd2lem  33870  dfufd2  33871  zringfrac  33875  deg1prod  33904  ply1dg3rt0irred  33905  r1plmhm  33930  r1pquslmic  33931  0mplrim  33935  mplidomlem  33948  extvfvcl  33957  mplmulmvr  33960  mplvrpmga  33966  psrgsum  33969  psrmonprod  33973  esplyfval3  33993  esplyfval1  33994  esplyfvaln  33995  esplyind  33996  exsslsb  34018  lindsunlem  34045  lindsun  34046  dimkerim  34048  fedgmullem1  34050  fedgmul  34052  dimlssid  34053  evls1fldgencl  34091  fldextrspunlsplem  34094  extdgfialg  34115  minplyirred  34132  fldext2chn  34149  constrmon  34165  constrconj  34166  constrfin  34167  constrelextdg2  34168  constrextdg2lem  34169  constrextdg2  34170  constrext2chnlem  34171  constrfiss  34172  cos9thpiminplylem2  34204  mdetpmtr1  34244  txomap  34255  qtophaus  34257  cmpcref  34271  zarclsun  34291  zarclssn  34294  zarcmplem  34302  pstmxmet  34318  sqsscirc1  34329  ordtrest2NEWlem  34343  ordtconnlem1  34345  pnfneige0  34372  lmxrge0  34373  lmdvg  34374  qqhval2  34403  esumcst  34484  esumrnmpt2  34489  esumfsup  34491  esumcvg  34507  esum2d  34514  esumiun  34515  sigaclfu2  34542  insiga  34559  ldsysgenld  34582  ldgenpisyslem1  34585  fiunelros  34596  measinb  34643  imambfm  34684  oms0  34719  omssubadd  34722  carsgclctunlem3  34742  eulerpartlemgvv  34798  dstrvprob  34894  signstfvneq0  34991  actfunsnrndisj  35024  reprinfz1  35041  breprexp  35052  afsval  35093  derangenlem  35684  sconnpi1  35752  cvmsss2  35787  cvmopnlem  35791  cvmlift3lem7  35838  msrval  36051  ifscgr  36557  cgrxfr  36568  btwnconn1lem13  36612  outsideofeu  36644  nmulcom  36707  nmuladdss  36726  neibastop2lem  36912  weiunso  37018  irrdifflemf  38010  irrdiff  38011  matunitlindflem1  38308  matunitlindflem2  38309  poimirlem14  38326  poimirlem22  38334  poimirlem29  38341  broucube  38346  heicant  38347  mblfinlem1  38349  itg2addnclem  38363  ftc1cnnc  38384  ftc1anclem7  38391  sstotbnd2  38466  equivtotbnd  38470  isbnd3  38476  ssbnd  38480  totbndbnd  38481  cntotbnd  38488  heibor1lem  38501  rrncmslem  38524  lssats  39827  lsat0cv  39848  lkrlss  39910  lfl1dim  39936  lfl1dim2N  39937  lkrpssN  39978  hlhgt2  40204  3dim2  40283  2dim  40285  lplncvrlvol  40431  paddasslem11  40645  pmapjat1  40668  2polssN  40730  pclfinclN  40765  pexmidlem8N  40792  lhpexle1lem  40822  4atex  40891  ltrnid  40950  trlator0  40986  cdlemg2cex  41406  tendodi1  41599  tendodi2  41600  diblss  41985  dihopelvalcpre  42063  dihatexv  42153  mapdval4N  42447  fldhmf1  42898  mndmolinv  42903  primrootscoprmpow  42907  posbezout  42908  primrootscoprbij2  42911  primrootspoweq0  42914  aks6d1c2p2  42927  hashscontpow  42930  aks6d1c2lem4  42935  aks6d1c2  42938  aks6d1c5  42947  sticksstones8  42961  sticksstones12  42966  sticksstones22  42976  aks6d1c6lem3  42980  aks6d1c6isolem1  42982  unitscyglem3  43005  aks5  43012  sn-subeu  43229  sn-0tie0  43266  fiabv  43345  frlmsnic  43349  fsuppind  43363  prjspersym  43380  dffltz  43407  nna4b4nsq  43433  mzpindd  43518  mzpsubst  43520  mzpcompact2lem  43523  eldioph2b  43535  irrapxlem3  43592  irrapxlem5  43594  pellex  43603  pell1234qrdich  43629  pell14qrexpcl  43635  congabseq  43742  jm2.26a  43768  jm2.26lem3  43769  rmydioph  43782  lnrfg  43887  hbt  43898  cantnftermord  44088  cantnfresb  44092  cantnf2  44093  oawordex2  44094  omabs2  44100  tfsconcatfv  44109  tfsconcatrev  44116  ofoaass  44128  nadd2rabtr  44152  nadd1suc  44160  naddgeoa  44162  rfovcnvf1od  44771  clsk3nimkb  44807  ntrneiiso  44858  ntrneikb  44861  ntrneixb  44862  ntrneik3  44863  ntrneix3  44864  ntrneik13  44865  ntrneix13  44866  4an4132  45249  iunconnlem2  45684  modelaxrep  45731  fnchoice  45790  cncmpmax  45793  ssinc  45846  ssdec  45847  disjf1  45942  supxrge  46095  suplesup  46096  infxr  46123  infleinf  46128  unb2ltle  46170  rexabslelem  46173  uzub  46186  supminfxr  46219  climrec  46360  climsuse  46365  islptre  46376  addlimc  46403  0ellimcdiv  46404  limsuppnfdlem  46456  limsupub  46459  limsuppnflem  46465  limsupubuz  46468  climinf3  46471  limsupmnflem  46475  climxrre  46505  liminfreuzlem  46557  liminflimsupclim  46562  xlimliminflimsup  46617  icccncfext  46642  cncfiooicclem1  46648  fperdvper  46674  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvmptfprodlem  46699  dvmptfprod  46700  dvnprodlem2  46702  stoweidlem7  46762  stoweidlem34  46789  stoweidlem52  46807  stoweidlem60  46815  wallispilem3  46822  fourierdlem34  46896  fourierdlem38  46900  fourierdlem39  46901  fourierdlem48  46909  fourierdlem50  46911  fourierdlem51  46912  fourierdlem73  46934  fourierdlem76  46937  fourierdlem77  46938  fourierdlem80  46941  fourierdlem87  46948  fourierdlem103  46964  fourierdlem104  46965  etransclem32  47021  etransclem33  47022  sge0f1o  47137  sge0pr  47149  sge0isum  47182  iundjiun  47215  meaiininclem  47241  hoicvr  47303  pimdecfgtioo  47472  pimincfltioo  47473  preimageiingt  47475  preimaleiinlt  47476  smflimlem2  47527  smflimlem4  47529  smfmullem3  47548  smflimmpt  47565  smfinflem  47572  smfpimne2  47595  fsupdm  47597  finfdm  47601  cfsetsnfsetfo  47838  funressnbrafv2  48022  imasetpreimafvbijlemf1  48194  bgoldbtbndlem2  48612  bgoldbtbndlem3  48613  bgoldbtbnd  48615  isuspgrim  48702  stgrusgra  48765  isubgr3stgrlem6  48777  2zlidl  49046  lindslinindsimp2  49284  snlindsntor  49292  lincresunit2  49299  islindeps2  49304  imaf1co  49974  imasubc3  49975  fucofvalg  50137  fuco21  50155  precofvalALT  50187  lanfval  50432  ranfval  50433