Theorem simpllr 773

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  frpomin  6279  fsnex  7211  soisoi  7255  f1o2ndf1  8030  fimaproj  8043  fprlem2  8187  tz7.49  8346  omabs  8552  omxpenlem  8938  fopwdom  8945  findcard3  9150  findcard3OLD  9151  frfi  9153  finsschain  9224  marypha1lem  9290  wemappo  9406  wdomtr  9432  cantnfp1  9538  ttrcltr  9573  harcard  9835  numacn  9906  infunsdom1  10070  sornom  10134  ssfin4  10167  fin1a2lem11  10267  fin1a2lem13  10269  fpwwe2lem12  10499  pwfseq  10521  mulcmpblnr  10928  00id  11251  addid1  11256  cnegex  11257  negeu  11312  add20  11588  ltmul12a  11932  lediv12a  11969  cru  12066  qextltlem  13037  xleadd1a  13088  xmullem  13099  xlemul1a  13123  ixxss12  13200  ioodisj  13315  fsuppmapnn0fz  13817  seqf1o  13865  mulexpz  13924  leexp1a  13994  faclbnd  14105  swrdswrdlem  14515  abs3lem  15149  rexico  15164  cau3lem  15165  rlim3  15306  ello12  15324  lo1bdd2  15332  elo12  15335  rlimconst  15352  isercoll  15478  climcau  15481  climbdd  15482  summolem2  15527  fsumconst  15601  o1fsum  15624  incexclem  15647  fprodconst  15787  bitsfzo  16241  dvdsmulgcd  16362  pc2dvds  16677  pcz  16679  pcadd  16687  pcfac  16697  vdwmc2  16777  vdwlem2  16780  vdwlem10  16788  vdw  16792  ramcl  16827  sbcie3s  16960  firest  17240  prdsval  17263  mreexd  17448  mreexexlemd  17450  iscat  17478  cidfval  17482  iscatd2  17487  catcocl  17491  catass  17492  catpropd  17515  cidpropd  17516  moni  17545  monpropd  17546  issubc  17647  subccocl  17657  funcco  17683  funcpropd  17713  fullpropd  17733  nati  17768  natpropd  17791  fucpropd  17792  xpcpropd  18023  curfuncf  18053  curf2ndf  18062  yonffthlem  18097  acsfiindd  18368  mndpropd  18507  mhmeql  18561  smndex1mgm  18642  isgrpinv  18728  dfgrp3lem  18769  mhmmnd  18793  cycsubm  18917  cycsubmcom  18919  conjnmzb  18965  gass  19003  symgextf  19121  dfod2  19267  gexdvds  19285  sylow3lem2  19329  efgredlem  19448  efgredeu  19453  ghmcmn  19528  oddvdssubg  19551  dprdfcntz  19713  pgpfaclem3  19781  issrg  19838  isring  19882  dvdsrmul1  19990  issubdrg  20154  islmhm2  20406  lmhmeql  20423  lssacsex  20512  isphl  20939  uvcf1  21105  lindfmm  21140  issubassa2  21202  opsrval  21353  mhpmulcl  21445  scmatmats  21766  smatvscl  21779  mdetunilem7  21873  gsummatr01lem4  21913  m2cpmfo  22011  pmatcollpw3fi1lem1  22041  pm2mpf1lem  22049  pm2mpf1  22054  mp2pm2mplem4  22064  pm2mpghm  22071  chfacfscmulfsupp  22114  chfacfpmmulfsupp  22118  cctop  22262  neiptoptop  22388  neiptopreu  22390  tgrest  22416  ordtrest2lem  22460  cnss1  22533  cncnp  22537  isnrm3  22616  uncmp  22660  cmpfi  22665  iunconn  22685  1stcrest  22710  subislly  22738  islly2  22741  cldllycmp  22752  lly1stc  22753  llycmpkgen2  22807  kgencn  22813  xkoccn  22876  ptcnplem  22878  pthaus  22895  txhaus  22904  txkgen  22909  xkohaus  22910  xkococnlem  22916  txconn  22946  regr1lem2  22997  kqreglem1  22998  reghmph  23050  nrmhmph  23051  trfil2  23144  ufileu  23176  flimopn  23232  flimcf  23239  fclscf  23282  ufilcmp  23289  cnpfcf  23298  cnextfun  23321  tgpmulg  23350  symgtgp  23363  tgpt0  23376  qustgplem  23378  ustex2sym  23474  ustex3sym  23475  trust  23487  restutop  23495  restutopopn  23496  ustuqtop4  23502  utop3cls  23509  utopreg  23510  cstucnd  23542  ucncn  23543  trcfilu  23552  neipcfilu  23554  ismet2  23592  metequiv2  23772  metcnp  23803  metcnp2  23804  metcnpi3  23808  txmetcnp  23809  metustto  23815  metustsym  23817  metust  23820  cfilucfil  23821  metuel2  23827  psmetutop  23829  restmetu  23832  metucn  23833  ngptgp  23898  tngngp  23924  nmoleub  24001  icccmp  24094  reconnlem2  24096  reconn  24097  xmetdcn2  24106  metdseq0  24123  metdscn  24125  elcncf2  24159  cncfmet  24178  cnheibor  24224  nmoleub2lem2  24385  nmoleub3  24388  cvsi  24399  iscfil2  24536  iscfil3  24543  cfilfcls  24544  equivcfil  24569  caubl  24578  bcthlem5  24598  pmltpc  24720  ovollb2  24759  ovoliunnul  24777  ovolicc2lem4  24790  volsup  24826  ioorf  24843  dyadss  24864  dyaddisjlem  24865  mbfposr  24922  cncombf  24928  mbflimsup  24936  i1fmulclem  24973  mbfi1fseqlem4  24989  iblss2  25076  ellimc2  25147  ellimc3  25149  dvnadd  25199  dvmptfsum  25245  dvferm1  25255  dvferm2  25257  fta1g  25438  plyeq0lem  25477  plydivex  25563  fta1  25574  aalioulem2  25599  aalioulem3  25600  ulmuni  25657  ulmbdd  25663  ulmdvlem3  25667  mtest  25669  abelthlem8  25704  efopn  25919  cxpmul2z  25952  cxpcn3lem  26006  jensen  26244  lgambdd  26292  lgamucov  26293  isppw2  26370  mersenne  26481  dchrelbas3  26492  dchrptlem1  26518  dchrpt  26521  lgsval2lem  26561  lgsdchrval  26608  lgsquad3  26641  2sqb  26686  2sqmo  26691  pntrsumbnd2  26821  pntpbnd  26842  pntibnd  26847  nosupno  26957  noinfno  26972  noetasuplem4  26990  noetalem1  26995  istrkgc  27104  istrkgb  27105  tgjustr  27124  tglowdim1i  27151  tgbtwndiff  27156  tgifscgr  27158  iscgrglt  27164  tgcgrxfr  27168  lnext  27217  tgbtwnconn1lem3  27224  tgbtwnconn1  27225  legval  27234  legov  27235  legov2  27236  legtrd  27239  legtri3  27240  legso  27249  hlcgrex  27266  hlcgreu  27268  tglnne  27278  tglndim0  27279  tglineeltr  27281  tglinethru  27286  tglnne0  27290  tglnpt2  27291  colline  27299  tglowdim2l  27300  tglowdim2ln  27301  mirreu3  27304  miriso  27320  midexlem  27342  isperp  27362  perpcom  27363  perpneq  27364  isperp2  27365  footexALT  27368  footex  27371  colperpexlem3  27382  opphllem  27385  midex  27387  oppne3  27393  opptgdim2  27395  opphllem2  27398  opphllem3  27399  opphllem5  27401  opphllem6  27402  opphl  27404  outpasch  27405  lnopp2hpgb  27413  colopp  27419  lmieu  27434  trgcopy  27454  trgcopyeu  27456  iscgra1  27460  cgrane1  27462  cgrane2  27463  cgrane3  27464  cgrahl1  27466  cgrahl2  27467  cgracgr  27468  cgraswap  27470  cgracom  27472  cgratr  27473  flatcgra  27474  cgrabtwn  27476  cgrahl  27477  dfcgra2  27480  sacgr  27481  acopyeu  27484  inaghl  27495  cgrg3col4  27503  f1otrg  27521  f1otrge  27522  axsegcon  27584  axeuclidlem  27619  upgr1eopALT  27776  usgr1eop  27906  pthdepisspth  28391  wpthswwlks2on  28614  clwwlkf1  28701  clwwlknscsh  28714  2pthfrgr  28936  n4cyclfrgr  28943  frgrwopreglem5  28973  frgrwopreglem5ALT  28974  friendshipgt3  29050  smcnlem  29347  0lno  29440  ubthlem1  29520  ubthlem3  29522  chocunii  29951  occl  29954  5oalem1  30304  3oalem2  30313  nmopub2tALT  30559  nmfnleub2  30576  lnconi  30683  kbass5  30770  mdslmd1lem1  30975  mdslmd1lem2  30976  cdj1i  31083  opreu2reuALT  31113  disjabrex  31208  disjabrexf  31209  2ndresdju  31273  acunirnmpt  31283  acunirnmpt2  31284  acunirnmpt2f  31285  aciunf1lem  31286  fnpreimac  31295  fgreu  31296  suppovss  31304  xrge0infss  31370  xrofsup  31377  fsumiunle  31430  s3f1  31508  ccatf1  31510  swrdf1  31515  ressprs  31528  dfmgc2  31561  mgcf1o  31568  xrge0addgt0  31587  gsumle  31637  psgnfzto1stlem  31654  fzto1st1  31656  cycpmco2  31687  cycpmrn  31697  cyc3genpm  31706  cycpmconjs  31710  cyc3conja  31711  submarchi  31727  isarchi3  31728  archiabllem1  31734  archiabllem2a  31735  suborng  31814  isarchiofld  31816  imaslmod  31849  nsgqusf1olem2  31896  intlidl  31899  rhmpreimaidl  31900  elrspunidl  31903  rhmimaidl  31906  prmidl2  31913  isprmidlc  31920  rhmpreimaprmidl  31924  qsidomlem2  31926  mxidlprm  31937  ssmxidl  31939  lindsunlem  32003  lindsun  32004  dimkerim  32006  fedgmullem1  32008  fedgmul  32010  mdetpmtr1  32071  txomap  32082  qtophaus  32084  cmpcref  32098  zarclsun  32118  zarclssn  32121  zarcmplem  32129  pstmxmet  32145  sqsscirc1  32156  ordtrest2NEWlem  32170  ordtconnlem1  32172  pnfneige0  32199  lmxrge0  32200  lmdvg  32201  qqhval2  32230  esumcst  32329  esumrnmpt2  32334  esumfsup  32336  esumcvg  32352  esum2d  32359  esumiun  32360  sigaclfu2  32387  insiga  32403  ldsysgenld  32426  ldgenpisyslem1  32429  fiunelros  32440  measinb  32487  imambfm  32529  oms0  32564  omssubadd  32567  carsgclctunlem3  32587  eulerpartlemgvv  32643  dstrvprob  32738  sgnsub  32811  signstfvneq0  32851  actfunsnrndisj  32885  reprinfz1  32902  breprexp  32913  afsval  32951  derangenlem  33432  sconnpi1  33500  cvmsss2  33535  cvmopnlem  33539  cvmlift3lem7  33586  msrval  33799  naddssim  34116  madebday  34176  cofcutr  34188  ifscgr  34442  cgrxfr  34453  btwnconn1lem13  34497  outsideofeu  34529  neibastop2lem  34645  irrdifflemf  35601  irrdiff  35602  matunitlindflem1  35878  matunitlindflem2  35879  poimirlem14  35896  poimirlem22  35904  poimirlem29  35911  broucube  35916  heicant  35917  mblfinlem1  35919  itg2addnclem  35933  ftc1cnnc  35954  ftc1anclem7  35961  sstotbnd2  36037  equivtotbnd  36041  isbnd3  36047  ssbnd  36051  totbndbnd  36052  cntotbnd  36059  heibor1lem  36072  rrncmslem  36095  lssats  37279  lsat0cv  37300  lkrlss  37362  lfl1dim  37388  lfl1dim2N  37389  lkrpssN  37430  hlhgt2  37657  3dim2  37736  2dim  37738  lplncvrlvol  37884  paddasslem11  38098  pmapjat1  38121  2polssN  38183  pclfinclN  38218  pexmidlem8N  38245  lhpexle1lem  38275  4atex  38344  ltrnid  38403  trlator0  38439  cdlemg2cex  38859  tendodi1  39052  tendodi2  39053  diblss  39438  dihopelvalcpre  39516  dihatexv  39606  mapdval4N  39900  fldhmf1  40352  aks6d1c2p2  40354  sticksstones8  40366  sticksstones12  40371  sticksstones22  40381  metakunt1  40382  metakunt2  40383  frlmsnic  40523  fsuppind  40539  sn-subeu  40668  sn-0tie0  40681  prjspersym  40706  dffltz  40733  nna4b4nsq  40759  mzpindd  40830  mzpsubst  40832  mzpcompact2lem  40835  eldioph2b  40847  irrapxlem3  40908  irrapxlem5  40910  pellex  40919  pell1234qrdich  40945  pell14qrexpcl  40951  congabseq  41059  jm2.26a  41085  jm2.26lem3  41086  rmydioph  41099  lnrfg  41207  hbt  41218  oawordex2  41312  omabs2  41317  ofoaass  41326  rfovcnvf1od  41933  clsk3nimkb  41971  ntrneiiso  42022  ntrneikb  42025  ntrneixb  42026  ntrneik3  42027  ntrneix3  42028  ntrneik13  42029  ntrneix13  42030  4an4132  42440  iunconnlem2  42876  fnchoice  42893  cncmpmax  42896  ssinc  42957  ssdec  42958  disjf1  43047  supxrge  43212  suplesup  43213  infxr  43241  infleinf  43246  unb2ltle  43290  rexabslelem  43293  uzub  43306  supminfxr  43339  climrec  43480  climsuse  43485  islptre  43496  addlimc  43525  0ellimcdiv  43526  limsuppnfdlem  43578  limsupub  43581  limsuppnflem  43587  limsupubuz  43590  climinf3  43593  limsupmnflem  43597  climxrre  43627  liminfreuzlem  43679  liminflimsupclim  43684  xlimliminflimsup  43739  icccncfext  43764  cncfiooicclem1  43770  fperdvper  43796  ioodvbdlimc1lem2  43809  ioodvbdlimc2lem  43811  dvmptfprodlem  43821  dvmptfprod  43822  dvnprodlem2  43824  stoweidlem7  43884  stoweidlem34  43911  stoweidlem52  43929  stoweidlem60  43937  wallispilem3  43944  fourierdlem34  44018  fourierdlem38  44022  fourierdlem39  44023  fourierdlem48  44031  fourierdlem50  44033  fourierdlem51  44034  fourierdlem73  44056  fourierdlem76  44059  fourierdlem77  44060  fourierdlem80  44063  fourierdlem87  44070  fourierdlem103  44086  fourierdlem104  44087  etransclem32  44143  etransclem33  44144  sge0f1o  44257  sge0pr  44269  sge0isum  44302  iundjiun  44335  meaiininclem  44361  pimdecfgtioo  44592  pimincfltioo  44593  preimageiingt  44595  preimaleiinlt  44596  smflimlem2  44647  smflimlem4  44649  smfmullem3  44668  smflimmpt  44685  smfinflem  44692  smfpimne2  44715  cfsetsnfsetfo  44905  funressnbrafv2  45087  imasetpreimafvbijlemf1  45207  bgoldbtbndlem2  45609  bgoldbtbndlem3  45610  bgoldbtbnd  45612  isomuspgrlem2  45636  mgmhmeql  45708  isrng  45785  2zlidl  45843  lindslinindsimp2  46155  snlindsntor  46163  lincresunit2  46170  islindeps2  46175