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  6342  fsnex  7288  soisoi  7333  f1o2ndf1  8123  fimaproj  8137  fprlem2  8304  tz7.49  8438  omabs  8643  cofon1  8664  naddssim  8678  omxpenlem  9080  fopwdom  9087  findcard3  9257  frfi  9259  finsschain  9330  marypha1lem  9407  wemappo  9525  wdomtr  9551  cantnfp1  9664  ttrcltr  9699  harcard  9987  numacn  10056  infunsdom1  10218  sornom  10283  ssfin4  10316  fin1a2lem11  10416  fin1a2lem13  10418  fpwwe2lem12  10655  pwfseq  10677  mulcmpblnr  11084  00id  11413  addrid  11418  cnegex  11419  negeu  11475  add20  11754  ltmul12a  12099  lediv12a  12136  cru  12238  qextltlem  13258  xleadd1a  13309  xmullem  13320  xlemul1a  13344  ixxss12  13422  ioodisj  13539  fvf1tp  13854  fsuppmapnn0fz  14064  seqf1o  14111  mulexpz  14170  leexp1a  14243  faclbnd  14358  ccatf1  14660  swrdf1  14723  swrdswrdlem  14777  s3rex  15025  sgnsub  15183  abs3lem  15430  rexico  15445  cau3lem  15446  rlim3  15589  ello12  15607  lo1bdd2  15615  elo12  15618  rlimconst  15635  isercoll  15759  climcau  15762  climbdd  15763  summolem2  15806  fsumconst  15880  o1fsum  15904  incexclem  15929  fprodconst  16071  bitsfzo  16531  dvdsmulgcd  16652  pc2dvds  16977  pcz  16979  pcadd  16987  pcfac  16997  vdwmc2  17077  vdwlem2  17080  vdwlem10  17088  vdw  17092  ramcl  17127  sbcie3s  17260  firest  17523  prdsval  17546  mreexd  17736  mreexexlemd  17738  iscat  17766  cidfval  17770  iscatd2  17775  catcocl  17779  catass  17780  catpropd  17803  cidpropd  17804  moni  17831  monpropd  17832  issubc  17930  subccocl  17940  funcco  17966  funcpropd  17997  fullpropd  18017  nati  18053  natpropd  18074  fucpropd  18075  xpcpropd  18302  curfuncf  18332  curf2ndf  18341  yonffthlem  18376  acsfiindd  18647  chnind  18715  chnso  18718  mgmhmeql  18824  sgrppropd  18839  mndpropd  18870  mhmeql  18941  smndex1mgm  19025  isgrpinv  19123  dfgrp3lem  19167  mhmmnd  19193  cycsubm  19336  cycsubmcom  19338  conjnmzb  19386  ghmqusnsg  19415  ghmquskerlem3  19419  ghmqusker  19420  gass  19434  symgextf  19550  dfod2  19697  gexdvds  19717  sylow3lem2  19761  efgredlem  19880  efgredeu  19885  ghmcmn  19964  oddvdssubg  19988  dprdfcntz  20150  pgpfaclem3  20218  gsumle  20278  isrng  20295  issrg  20333  isring  20382  dvdsrmul1  20516  isdrng4  20908  issubdrg  20952  suborng  21048  islmhm2  21228  lmhmeql  21245  lssacsex  21337  rhmpreimaidl  21485  rhmqusnsg  21494  prmidl2  21535  isprmidlc  21541  rhmpreimaprmidl  21548  qsidomlem2  21550  ssdifidllem  21553  ssdifidlprm  21555  isphl  21847  uvcf1  22011  lindfmm  22046  sraassab  22089  issubassa2  22113  opsrval  22268  psdmul  22400  scmatmats  22739  smatvscl  22752  mdetunilem7  22846  gsummatr01lem4  22886  matunitlindflem1  22907  matunitlindflem2  22908  m2cpmfo  22987  pmatcollpw3fi1lem1  23017  pm2mpf1lem  23025  pm2mpf1  23030  mp2pm2mplem4  23040  pm2mpghm  23047  chfacfscmulfsupp  23090  chfacfpmmulfsupp  23094  cctop  23237  neiptoptop  23362  neiptopreu  23364  tgrest  23390  ordtrest2lem  23434  cnss1  23507  cncnp  23511  isnrm3  23590  uncmp  23634  cmpfi  23639  iunconn  23659  1stcrest  23684  subislly  23713  islly2  23716  cldllycmp  23727  lly1stc  23728  llycmpkgen2  23782  kgencn  23788  xkoccn  23851  ptcnplem  23853  pthaus  23870  txhaus  23879  txkgen  23884  xkohaus  23885  xkococnlem  23891  txconn  23921  regr1lem2  23972  kqreglem1  23973  reghmph  24025  nrmhmph  24026  trfil2  24119  ufileu  24151  flimopn  24207  flimcf  24214  fclscf  24257  ufilcmp  24264  cnpfcf  24273  cnextfun  24296  tgpmulg  24325  symgtgp  24338  tgpt0  24351  qustgplem  24353  ustex2sym  24449  ustex3sym  24450  trust  24461  restutop  24469  restutopopn  24470  ustuqtop4  24476  utop3cls  24483  utopreg  24484  cstucnd  24515  ucncn  24516  trcfilu  24525  neipcfilu  24527  ismet2  24565  metequiv2  24742  metcnp  24773  metcnp2  24774  metcnpi3  24778  txmetcnp  24779  metustto  24785  metustsym  24787  metust  24790  cfilucfil  24791  metuel2  24797  psmetutop  24799  restmetu  24802  metucn  24803  ngptgp  24868  tngngp  24886  nmoleub  24963  icccmp  25058  reconnlem2  25060  reconn  25061  xmetdcn2  25070  metdseq0  25087  metdscn  25089  elcncf2  25124  cncfmet  25143  cnheibor  25189  nmoleub2lem2  25350  nmoleub3  25353  cvsi  25364  iscfil2  25500  iscfil3  25507  cfilfcls  25508  equivcfil  25533  caubl  25542  bcthlem5  25562  pmltpc  25684  ovollb2  25723  ovoliunnul  25741  ovolicc2lem4  25754  volsup  25790  ioorf  25807  dyadss  25828  dyaddisjlem  25829  mbfposr  25886  cncombf  25892  mbflimsup  25900  i1fmulclem  25936  mbfi1fseqlem4  25952  iblss2  26040  ellimc2  26111  ellimc3  26113  dvnadd  26163  dvmptfsum  26209  dvferm1  26219  dvferm2  26221  fta1g  26402  plyeq0lem  26443  plydivex  26534  fta1  26545  aalioulem2  26576  aalioulem3  26577  ulmuni  26635  ulmbdd  26641  ulmdvlem3  26645  mtest  26647  abelthlem8  26682  efopn  26903  cxpmul2z  26936  cxpcn3lem  26992  jensen  27233  lgambdd  27281  lgamucov  27282  isppw2  27359  mersenne  27471  dchrelbas3  27482  dchrptlem1  27508  dchrpt  27511  lgsval2lem  27551  lgsdchrval  27598  lgsquad3  27631  2sqb  27676  2sqmo  27681  pntrsumbnd2  27811  pntpbnd  27832  pntibnd  27837  nosupno  27947  noinfno  27962  noetasuplem4  27980  noetalem1  27985  madebday  28173  cofcutr  28197  negsprop  28308  mulscom  28412  absmuls  28517  addonbday  28552  bdayfinbndlem1  28740  z12sge0  28756  remulscl  28775  tgjustr  28823  tgsegconeu  28836  tglowdim1i  28851  tgbtwndiff  28856  tgifscgr  28858  iscgrglt  28864  tgcgrxfr  28868  lnext  28917  tgbtwnconn1lem3  28924  tgbtwnconn1  28925  legval  28934  legov  28935  legov2  28936  legtrd  28939  legtri3  28940  legso  28949  hlcgrex  28969  hlcgreu  28971  tglnne  28983  tglndim0  28984  tglineeltr  28986  tglinethru  28991  tglinesseq  28995  tglnne0  28996  colline  29005  tglowdim2l  29006  tglowdim2ln  29007  tglnpt2  29008  tglnpt3  29009  tglnpt4  29010  mirreu3  29013  miriso  29029  midexlem  29051  isperp  29074  perpcom  29075  perpneq  29076  isperp2  29077  footexALT  29080  footex  29083  colperpexlem3  29095  opphllem  29098  midex  29100  oppne3  29106  opptgdim2  29108  opphllem2  29111  opphllem3  29112  opphllem5  29114  opphllem6  29115  opphl  29117  outpasch  29120  lnopp2hpgb  29128  colopp  29134  plngrnssp  29144  lnincplng  29149  plngrotlem1  29152  plngrotlem3  29154  lnssplng  29157  plng3p  29162  lmieu  29176  trgcopy  29198  trgcopyeu  29200  iscgra1  29204  cgrane1  29206  cgrane2  29207  cgrane3  29208  cgrahl1  29210  cgrahl2  29211  cgracgr  29212  cgraswap  29214  cgracom  29216  cgratr  29217  zerocgra  29218  flatcgra  29219  cgrabtwn  29221  cgrahl  29222  dfcgra2  29225  sacgr  29226  acopyeu  29229  ragcgra  29230  cgrarag  29231  ragsupplcgra  29232  tgaaddcpbllem1  29236  tgaaddcpbllem3  29238  tgaaddcpbl  29239  inaghl  29251  cgrg3col4  29259  cgraer  29264  cgrabasimass  29265  angmgmaddeu1  29266  angmgmaddeu2  29267  angmgmaddeu3  29268  angmgmaddeu4  29269  angmgmaddeu5  29270  angmgmaddeu6  29271  angmgmaddeu7  29272  angmgmaddov2lem  29274  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddlid  29279  angmgmaddrid  29280  angmgm  29284  prlnghpg  29311  dfprlng2  29312  dfprlng3  29313  perpprlng  29315  prlngex  29316  prlngmolem1  29317  prlngmolem2  29318  prlngmo2  29321  prlngplngtr  29324  quadcgrprlng  29331  f1otrg  29335  f1otrge  29336  axsegcon  29392  axeuclidlem  29427  upgr1eopALT  29582  usgr1eop  29718  pthdepisspth  30208  wpthswwlks2on  30440  clwwlkf1  30527  clwwlknscsh  30540  2pthfrgr  30772  n4cyclfrgr  30779  frgrwopreglem5  30809  frgrwopreglem5ALT  30810  friendshipgt3  30886  smcnlem  31186  0lno  31279  ubthlem1  31359  ubthlem3  31361  chocunii  31790  occl  31793  5oalem1  32143  3oalem2  32152  nmopub2tALT  32398  nmfnleub2  32415  lnconi  32522  kbass5  32609  mdslmd1lem1  32814  mdslmd1lem2  32815  cdj1i  32922  opreu2reuALT  32960  disjabrex  33063  disjabrexf  33064  2ndresdju  33130  acunirnmpt  33140  acunirnmpt2  33141  acunirnmpt2f  33142  aciunf1lem  33143  fnpreimac  33151  fgreu  33152  suppovss  33161  xrge0infss  33239  xrofsup  33246  elq2  33290  fsumiunle  33307  2exple2exp  33312  s3f1  33398  ccatws1f1o  33401  ressprs  33414  dfmgc2  33444  mgcf1o  33451  xrge0addgt0  33465  mndlrinvb  33473  mndlactf1  33474  mndlactfo  33475  mndractf1  33476  mndractfo  33477  mndlactf1o  33478  gsumfs2d  33509  suppgsumssiun  33520  gsumwun  33524  gsumwrd2dccatlem  33525  psgnfzto1stlem  33548  fzto1st1  33550  cycpmco2  33581  cycpmrn  33591  cyc3genpm  33600  cycpmconjs  33604  cyc3conja  33605  conjga  33618  fxpsubrg  33622  submarchi  33634  isarchi3  33635  archiabllem1  33641  archiabllem2a  33642  isarchiofld  33647  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem4  33693  elrgspnsubrunlem2  33696  erler  33713  rlocaddval  33717  rlocmulval  33718  rloccring  33719  rloc1r  33721  rlocisunit  33724  subrdom  33733  ricdomn1  33737  fracfld  33757  imaslmod  33801  dvdsruasso  33826  unitprodclb  33830  nsgqusf1olem2  33851  lmhmqusker  33854  intlidl  33856  rhmquskerlem  33861  elrspunidl  33864  elrspunsn  33865  rhmimaidl  33868  mxidlprm  33881  ssmxidl  33885  opprqusplusg  33899  opprqusmulr  33901  qsdrngilem  33904  qsdrngi  33905  drnglring  33910  dflring2  33911  dflringlem2  33913  rsprprmprmidl  33940  rsprprmprmidlb  33941  rprmirred  33949  rprmirredb  33950  rprmdvdspow  33951  rprmdvdsprod  33952  1arithidom  33955  1arithufdlem2  33963  1arithufdlem3  33964  1arithufdlem4  33965  dfufd2lem  33967  dfufd2  33968  zringfrac  33972  deg1prod  34001  ply1dg3rt0irred  34002  r1plmhm  34027  r1pquslmic  34028  0mplrim  34032  mplidomlem  34045  extvfvcl  34054  mplmulmvr  34057  mplvrpmga  34063  psrgsum  34066  psrmonprod  34070  esplyfval3  34090  esplyfval1  34091  esplyfvaln  34092  esplyind  34093  exsslsb  34115  lindsunlem  34142  lindsun  34143  dimkerim  34145  fedgmullem1  34147  fedgmul  34149  dimlssid  34150  evls1fldgencl  34188  fldextrspunlsplem  34191  extdgfialg  34212  minplyirred  34229  fldext2chn  34246  constrmon  34262  constrconj  34263  constrfin  34264  constrelextdg2  34265  constrextdg2lem  34266  constrextdg2  34267  constrext2chnlem  34268  constrfiss  34269  cos9thpiminplylem2  34301  mdetpmtr1  34341  txomap  34352  qtophaus  34354  cmpcref  34368  zarclsun  34388  zarclssn  34391  zarcmplem  34399  pstmxmet  34415  sqsscirc1  34426  ordtrest2NEWlem  34440  ordtconnlem1  34442  pnfneige0  34469  lmxrge0  34470  lmdvg  34471  qqhval2  34500  esumcst  34581  esumrnmpt2  34586  esumfsup  34588  esumcvg  34604  esum2d  34611  esumiun  34612  sigaclfu2  34639  insiga  34656  ldsysgenld  34679  ldgenpisyslem1  34682  fiunelros  34693  measinb  34740  imambfm  34781  oms0  34816  omssubadd  34819  carsgclctunlem3  34839  eulerpartlemgvv  34895  dstrvprob  34991  signstfvneq0  35088  actfunsnrndisj  35121  reprinfz1  35138  breprexp  35149  afsval  35190  derangenlem  35758  sconnpi1  35826  cvmsss2  35861  cvmopnlem  35865  cvmlift3lem7  35912  msrval  36125  ifscgr  36632  cgrxfr  36643  btwnconn1lem13  36687  outsideofeu  36719  nmulcom  36782  nmuladdss  36801  neibastop2lem  36987  weiunso  37093  irrdifflemf  38085  irrdiff  38086  poimirlem14  38391  poimirlem22  38399  poimirlem29  38406  broucube  38411  heicant  38412  mblfinlem1  38414  itg2addnclem  38428  ftc1cnnc  38449  ftc1anclem7  38456  sstotbnd2  38532  equivtotbnd  38536  isbnd3  38542  ssbnd  38546  totbndbnd  38547  cntotbnd  38554  heibor1lem  38567  rrncmslem  38590  lssats  39893  lsat0cv  39914  lkrlss  39976  lfl1dim  40002  lfl1dim2N  40003  lkrpssN  40044  hlhgt2  40270  3dim2  40349  2dim  40351  lplncvrlvol  40497  paddasslem11  40711  pmapjat1  40734  2polssN  40796  pclfinclN  40831  pexmidlem8N  40858  lhpexle1lem  40888  4atex  40957  ltrnid  41016  trlator0  41052  cdlemg2cex  41472  tendodi1  41665  tendodi2  41666  diblss  42051  dihopelvalcpre  42129  dihatexv  42219  mapdval4N  42513  fldhmf1  42964  mndmolinv  42969  primrootscoprmpow  42973  posbezout  42974  primrootscoprbij2  42977  primrootspoweq0  42980  aks6d1c2p2  42993  hashscontpow  42996  aks6d1c2lem4  43001  aks6d1c2  43004  aks6d1c5  43013  sticksstones8  43027  sticksstones12  43032  sticksstones22  43042  aks6d1c6lem3  43046  aks6d1c6isolem1  43048  unitscyglem3  43071  aks5  43078  sn-subeu  43310  sn-0tie0  43347  fiabv  43426  frlmsnic  43430  fsuppind  43444  prjspersym  43461  dffltz  43488  nna4b4nsq  43514  mzpindd  43599  mzpsubst  43601  mzpcompact2lem  43604  eldioph2b  43616  irrapxlem3  43673  irrapxlem5  43675  pellex  43684  pell1234qrdich  43710  pell14qrexpcl  43716  congabseq  43823  jm2.26a  43849  jm2.26lem3  43850  rmydioph  43863  lnrfg  43968  hbt  43979  cantnftermord  44169  cantnfresb  44173  cantnf2  44174  oawordex2  44175  omabs2  44181  tfsconcatfv  44190  tfsconcatrev  44197  ofoaass  44209  nadd2rabtr  44233  nadd1suc  44241  naddgeoa  44243  rfovcnvf1od  44852  clsk3nimkb  44888  ntrneiiso  44939  ntrneikb  44942  ntrneixb  44943  ntrneik3  44944  ntrneix3  44945  ntrneik13  44946  ntrneix13  44947  4an4132  45330  iunconnlem2  45765  modelaxrep  45812  fnchoice  45871  cncmpmax  45874  ssinc  45927  ssdec  45928  disjf1  46023  supxrge  46176  suplesup  46177  infxr  46204  infleinf  46209  unb2ltle  46251  rexabslelem  46254  uzub  46267  supminfxr  46300  climrec  46441  climsuse  46446  islptre  46457  addlimc  46484  0ellimcdiv  46485  limsuppnfdlem  46537  limsupub  46540  limsuppnflem  46546  limsupubuz  46549  climinf3  46552  limsupmnflem  46556  climxrre  46586  liminfreuzlem  46638  liminflimsupclim  46643  xlimliminflimsup  46698  icccncfext  46723  cncfiooicclem1  46729  fperdvper  46755  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvmptfprodlem  46780  dvmptfprod  46781  dvnprodlem2  46783  stoweidlem7  46843  stoweidlem34  46870  stoweidlem52  46888  stoweidlem60  46896  wallispilem3  46903  fourierdlem34  46977  fourierdlem38  46981  fourierdlem39  46982  fourierdlem48  46990  fourierdlem50  46992  fourierdlem51  46993  fourierdlem73  47015  fourierdlem76  47018  fourierdlem77  47019  fourierdlem80  47022  fourierdlem87  47029  fourierdlem103  47045  fourierdlem104  47046  etransclem32  47102  etransclem33  47103  sge0f1o  47218  sge0pr  47230  sge0isum  47263  iundjiun  47296  meaiininclem  47322  hoicvr  47384  pimdecfgtioo  47553  pimincfltioo  47554  preimageiingt  47556  preimaleiinlt  47557  smflimlem2  47608  smflimlem4  47610  smfmullem3  47629  smflimmpt  47646  smfinflem  47653  smfpimne2  47676  fsupdm  47678  finfdm  47682  cfsetsnfsetfo  47956  funressnbrafv2  48140  imasetpreimafvbijlemf1  48312  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  bgoldbtbnd  48733  isuspgrim  48820  stgrusgra  48883  isubgr3stgrlem6  48895  2zlidl  49163  lindslinindsimp2  49401  snlindsntor  49409  lincresunit2  49416  islindeps2  49421  imaf1co  50089  imasubc3  50090  fucofvalg  50252  fuco21  50270  precofvalALT  50302  lanfval  50547  ranfval  50548