Theorem simpllr 784

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  simp-4rOLD  795  fsnex  6758  soisoi  6798  f1o2ndf1  7515  tz7.49  7772  omabs  7960  omxpenlem  8296  fopwdom  8303  findcard3  8438  frfi  8440  finsschain  8508  marypha1lem  8574  wdomtr  8715  cantnfp1  8821  harcard  9083  numacn  9151  infunsdom1  9316  cofsmo  9372  sornom  9380  ssfin4  9413  fin1a2lem11  9513  fin1a2lem13  9515  ttukeylem5  9616  fpwwe2lem13  9745  pwfseq  9767  mulcmpblnr  10173  00id  10492  addid1  10497  cnegex  10498  negeu  10552  add20  10821  ltmul12a  11160  lediv12a  11197  fiminre  11253  cru  11293  qextltlem  12247  xleadd1a  12297  xmullem  12308  xlemul1a  12332  ixxss12  12409  ioodisj  12521  fsuppmapnn0fz  13015  seqf1o  13061  mulexpz  13119  leexp1a  13138  faclbnd  13293  swrdswrdlem  13679  abs3lem  14297  cau3lem  14313  rlim3  14448  ello12  14466  lo1bdd2  14474  elo12  14477  rlimconst  14494  isercoll  14617  climcau  14620  climbdd  14621  summolem2  14666  fsumconst  14740  o1fsum  14763  incexclem  14786  fprodconst  14925  bitsfzo  15372  dvdsmulgcd  15489  pc2dvds  15796  pcz  15798  pcadd  15806  pcfac  15816  vdwmc2  15896  vdwlem2  15899  vdwlem10  15907  vdw  15911  ramcl  15946  sbcie3s  16124  firest  16294  prdsval  16316  mreexd  16503  mreexexlemd  16505  iscat  16533  cidfval  16537  iscatd2  16542  catcocl  16546  catass  16547  catpropd  16569  cidpropd  16570  moni  16596  monpropd  16597  issubc  16695  subccocl  16705  funcco  16731  funcpropd  16760  fullpropd  16780  nati  16815  natpropd  16836  fucpropd  16837  xpcpropd  17049  curfuncf  17079  curf2ndf  17088  yonffthlem  17123  acsfiindd  17378  mndpropd  17517  mhmeql  17565  isgrpinv  17673  dfgrp3lem  17714  mhmmnd  17738  conjnmzb  17893  gass  17931  symgextf  18034  dfod2  18178  gexdvds  18196  sylow3lem2  18240  efgredlem  18357  efgredeu  18362  ghmcmn  18434  oddvdssubg  18455  dprdfcntz  18612  pgpfaclem3  18680  issrg  18705  isring  18749  dvdsrmul1  18851  issubdrg  19005  islmhm2  19241  lmhmeql  19258  lssacsex  19348  issubassa2  19550  opsrval  19679  isphl  20179  uvcf1  20338  lindfmm  20373  scmatmats  20525  smatvscl  20538  mdetunilem7  20632  gsummatr01lem4  20673  m2cpmfo  20771  decpmatmulsumfsupp  20788  pmatcollpw3fi1lem1  20801  pm2mpf1lem  20809  pm2mpf1  20814  mp2pm2mplem4  20824  pm2mpghm  20831  pm2mpmhmlem1  20833  pm2mpmhmlem2  20834  chfacfscmulfsupp  20874  chfacfpmmulfsupp  20878  cctop  21021  neiptoptop  21146  neiptopreu  21148  tgrest  21174  ordtrest2lem  21218  cnss1  21291  cncnp  21295  isnrm3  21374  uncmp  21417  cmpfi  21422  iunconn  21442  1stcrest  21467  subislly  21495  islly2  21498  cldllycmp  21509  lly1stc  21510  llycmpkgen2  21564  kgencn  21570  xkoccn  21633  ptcnplem  21635  pthaus  21652  txhaus  21661  txkgen  21666  xkohaus  21667  xkococnlem  21673  txconn  21703  regr1lem2  21754  kqreglem1  21755  reghmph  21807  nrmhmph  21808  trfil2  21901  ufileu  21933  flimopn  21989  flimcf  21996  fclscf  22039  ufilcmp  22046  cnpfcf  22055  cnextfun  22078  tgpmulg  22107  symgtgp  22115  tgpt0  22132  qustgplem  22134  ustex2sym  22230  ustex3sym  22231  trust  22243  restutop  22251  restutopopn  22252  ustuqtop2  22256  ustuqtop4  22258  utop3cls  22265  utopreg  22266  cstucnd  22298  ucncn  22299  trcfilu  22308  neipcfilu  22310  ismet2  22348  metequiv2  22525  metcnp  22556  metcnp2  22557  metcnpi3  22561  txmetcnp  22562  metustto  22568  metustsym  22570  metust  22573  cfilucfil  22574  metuel2  22580  psmetutop  22582  restmetu  22585  metucn  22586  ngptgp  22650  tngngp  22668  nmoleub  22745  icccmp  22838  reconnlem2  22840  reconn  22841  xmetdcn2  22850  metdseq0  22867  metdscn  22869  elcncf2  22903  cncfmet  22921  cnheibor  22964  nmoleub2lem2  23125  nmoleub3  23128  cvsi  23139  iscfil2  23274  iscfil3  23281  cfilfcls  23282  equivcfil  23307  caubl  23316  bcthlem5  23335  pmltpc  23430  ovollb2  23469  ovoliunnul  23487  ovolicc2lem4  23500  volsup  23536  ioorf  23553  dyadss  23574  dyaddisjlem  23575  mbfposr  23632  cncombf  23638  mbflimsup  23646  i1fmulclem  23682  mbfi1fseqlem4  23698  iblss2  23785  ellimc2  23854  ellimc3  23856  dvnadd  23905  dvmptfsum  23951  dvferm1  23961  dvferm2  23963  fta1g  24140  plyeq0lem  24179  plydivex  24265  fta1  24276  aalioulem2  24301  aalioulem3  24302  ulmuni  24359  ulmbdd  24365  ulmdvlem3  24369  mtest  24371  abelthlem8  24406  pilem3OLD  24421  efopn  24617  cxpmul2z  24650  cxpcn3lem  24701  jensen  24928  lgambdd  24976  lgamucov  24977  isppw2  25054  sqf11  25078  mersenne  25165  dchrelbas3  25176  dchrptlem1  25202  dchrpt  25205  lgsval2lem  25245  lgsdchrval  25292  lgsquad3  25325  2sqb  25370  pntrsumbnd2  25469  pntpbnd  25490  pntibnd  25495  istrkgc  25566  istrkgb  25567  tglowdim1i  25609  tgbtwndiff  25614  tgifscgr  25616  iscgrglt  25622  tgcgrxfr  25626  lnext  25675  tgbtwnconn1lem3  25682  tgbtwnconn1  25683  legval  25692  legov  25693  legov2  25694  legtrd  25697  legtri3  25698  legso  25707  hlcgrex  25724  hlcgreu  25726  tglnne  25736  tglndim0  25737  tglineeltr  25739  tglinethru  25744  tglnne0  25748  tglnpt2  25749  colline  25757  tglowdim2l  25758  tglowdim2ln  25759  mirreu3  25762  miriso  25778  midexlem  25800  isperp  25820  perpcom  25821  perpneq  25822  isperp2  25823  footex  25826  colperpexlem3  25837  opphllem  25840  midex  25842  oppne3  25848  opptgdim2  25850  opphllem2  25853  opphllem3  25854  opphllem5  25856  opphllem6  25857  opphl  25859  outpasch  25860  lnopp2hpgb  25868  colopp  25874  lmieu  25889  trgcopy  25909  trgcopyeu  25911  iscgra1  25915  cgrane1  25917  cgrane2  25918  cgrane3  25919  cgrahl1  25921  cgrahl2  25922  cgracgr  25923  cgraswap  25925  cgracom  25927  cgratr  25928  cgrabtwn  25930  cgrahl  25931  dfcgra2  25934  sacgr  25935  acopyeu  25938  inaghl  25944  cgrg3col4  25947  f1otrg  25964  f1otrge  25965  axsegcon  26020  axeuclidlem  26055  axcontlem2  26058  upgr1eopALT  26225  usgr1eop  26357  pthdepisspth  26858  wpthswwlks2on  27101  clwwlkf1  27197  clwwlknscsh  27212  2pthfrgr  27458  n4cyclfrgr  27465  frgrwopreglem5  27495  frgrwopreglem5ALT  27496  friendshipgt3  27585  smcnlem  27879  0lno  27972  ubthlem1  28053  ubthlem3  28055  chocunii  28487  occl  28490  5oalem1  28840  3oalem2  28849  nmopub2tALT  29095  nmfnleub2  29112  lnconi  29219  kbass5  29306  mdslmd1lem1  29511  mdslmd1lem2  29512  cdj1i  29619  disjabrex  29719  disjabrexf  29720  acunirnmpt  29785  acunirnmpt2  29786  acunirnmpt2f  29787  aciunf1lem  29788  fgreu  29797  xrge0infss  29851  xrofsup  29859  fsumiunle  29901  2sqmo  29973  ressprs  29979  xrge0addgt0  30015  submarchi  30064  isarchi3  30065  archiabllem1  30071  archiabllem2a  30072  gsumle  30103  suborng  30139  isarchiofld  30141  psgnfzto1stlem  30174  fzto1st1  30176  mdetpmtr1  30213  fimaproj  30224  txomap  30225  qtophaus  30227  cmpcref  30241  pstmxmet  30264  sqsscirc1  30278  ordtrest2NEWlem  30292  ordtconnlem1  30294  pnfneige0  30321  lmxrge0  30322  lmdvg  30323  qqhval2  30350  esumcst  30449  esumrnmpt2  30454  esumfsup  30456  esumcvg  30472  esum2d  30479  esumiun  30480  sigaclfu2  30508  insiga  30524  ldsysgenld  30547  ldgenpisyslem1  30550  fiunelros  30561  measinb  30608  imambfm  30648  oms0  30683  omssubadd  30686  carsgclctunlem3  30706  eulerpartlemgvv  30762  dstrvprob  30857  sgnsub  30930  signstfvneq0  30973  actfunsnrndisj  31007  reprinfz1  31024  breprexp  31035  afsval  31073  derangenlem  31474  sconnpi1  31542  cvmsss2  31577  cvmopnlem  31581  cvmlift3lem7  31628  msrval  31756  frpomin  32057  nosupno  32168  noetalem3  32184  noetalem5  32186  ifscgr  32470  cgrxfr  32481  btwnconn1lem13  32525  outsideofeu  32557  neibastop2lem  32674  matunitlindflem1  33716  matunitlindflem2  33717  poimirlem14  33734  poimirlem22  33742  poimirlem29  33749  broucube  33754  heicant  33755  mblfinlem1  33757  itg2addnclem  33771  ftc1cnnc  33794  ftc1anclem7  33801  sstotbnd2  33882  equivtotbnd  33886  isbnd3  33892  ssbnd  33896  totbndbnd  33897  cntotbnd  33904  heibor1lem  33917  rrncmslem  33940  lssats  34790  lsat0cv  34811  lkrlss  34873  lfl1dim  34899  lfl1dim2N  34900  lkrpssN  34941  hlhgt2  35167  3dim2  35246  2dim  35248  lplncvrlvol  35394  paddasslem11  35608  pmapjat1  35631  2polssN  35693  pclfinclN  35728  pexmidlem8N  35755  lhpexle1lem  35785  4atex  35854  ltrnid  35913  trlator0  35949  cdlemg2cex  36369  tendodi1  36562  tendodi2  36563  diblss  36948  dihopelvalcpre  37026  dihatexv  37116  mapdval4N  37410  mzpindd  37808  mzpsubst  37810  mzpcompact2lem  37813  eldioph2b  37825  irrapxlem3  37887  irrapxlem5  37889  pellex  37898  pell1234qrdich  37924  pell14qrexpcl  37930  congabseq  38039  jm2.26a  38065  jm2.26lem3  38066  rmydioph  38079  lnrfg  38187  hbt  38198  rfovcnvf1od  38795  clsk3nimkb  38835  ntrneiiso  38886  ntrneikb  38889  ntrneixb  38890  ntrneik3  38891  ntrneix3  38892  ntrneik13  38893  ntrneix13  38894  4an4132  39200  iunconnlem2  39662  fnchoice  39679  cncmpmax  39682  ssinc  39754  ssdec  39755  disjf1  39855  supxrge  40031  suplesup  40032  infxr  40060  infleinf  40065  unb2ltle  40118  rexabslelem  40121  uzub  40134  supminfxr  40170  climrec  40312  climsuse  40317  islptre  40328  addlimc  40357  0ellimcdiv  40358  limsuppnfdlem  40410  limsupub  40413  limsuppnflem  40419  limsupubuz  40422  climinf3  40425  limsupmnflem  40429  climxrre  40459  liminfreuzlem  40511  liminflimsupclim  40516  icccncfext  40577  cncfiooicclem1  40583  fperdvper  40610  ioodvbdlimc1lem2  40624  ioodvbdlimc2lem  40626  dvmptfprodlem  40636  dvmptfprod  40637  dvnprodlem2  40639  stoweidlem7  40700  stoweidlem34  40727  stoweidlem52  40745  stoweidlem60  40753  wallispilem3  40760  fourierdlem34  40834  fourierdlem38  40838  fourierdlem39  40839  fourierdlem48  40847  fourierdlem50  40849  fourierdlem51  40850  fourierdlem73  40872  fourierdlem76  40875  fourierdlem77  40876  fourierdlem80  40879  fourierdlem87  40886  fourierdlem103  40902  fourierdlem104  40903  etransclem32  40959  etransclem33  40960  sge0f1o  41075  sge0pr  41087  sge0isum  41120  iundjiun  41153  meaiininclem  41179  pimdecfgtioo  41406  pimincfltioo  41407  preimageiingt  41409  preimaleiinlt  41410  smflimlem2  41459  smflimlem4  41461  smfmullem3  41479  smflimmpt  41495  smfinflem  41502  funressnbrafv2  41830  bgoldbtbndlem2  42266  bgoldbtbndlem3  42267  bgoldbtbnd  42269  mgmhmeql  42368  isrng  42441  2zlidl  42499  lindslinindsimp2  42817  snlindsntor  42825  lincresunit2  42832  islindeps2  42837