Theorem simpllr 775

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  frpomin  6339  fsnex  7278  soisoi  7322  f1o2ndf1  8105  fimaproj  8118  fprlem2  8283  tz7.49  8442  omabs  8647  cofon1  8668  naddssim  8681  omxpenlem  9070  fopwdom  9077  findcard3  9282  findcard3OLD  9283  frfi  9285  finsschain  9356  marypha1lem  9425  wemappo  9541  wdomtr  9567  cantnfp1  9673  ttrcltr  9708  harcard  9970  numacn  10041  infunsdom1  10205  sornom  10269  ssfin4  10302  fin1a2lem11  10402  fin1a2lem13  10404  fpwwe2lem12  10634  pwfseq  10656  mulcmpblnr  11063  00id  11386  addrid  11391  cnegex  11392  negeu  11447  add20  11723  ltmul12a  12067  lediv12a  12104  cru  12201  qextltlem  13178  xleadd1a  13229  xmullem  13240  xlemul1a  13264  ixxss12  13341  ioodisj  13456  fsuppmapnn0fz  13958  seqf1o  14006  mulexpz  14065  leexp1a  14137  faclbnd  14247  swrdswrdlem  14651  abs3lem  15282  rexico  15297  cau3lem  15298  rlim3  15439  ello12  15457  lo1bdd2  15465  elo12  15468  rlimconst  15485  isercoll  15611  climcau  15614  climbdd  15615  summolem2  15659  fsumconst  15733  o1fsum  15756  incexclem  15779  fprodconst  15919  bitsfzo  16373  dvdsmulgcd  16494  pc2dvds  16809  pcz  16811  pcadd  16819  pcfac  16829  vdwmc2  16909  vdwlem2  16912  vdwlem10  16920  vdw  16924  ramcl  16959  sbcie3s  17092  firest  17375  prdsval  17398  mreexd  17583  mreexexlemd  17585  iscat  17613  cidfval  17617  iscatd2  17622  catcocl  17626  catass  17627  catpropd  17650  cidpropd  17651  moni  17680  monpropd  17681  issubc  17782  subccocl  17792  funcco  17818  funcpropd  17848  fullpropd  17868  nati  17903  natpropd  17926  fucpropd  17927  xpcpropd  18158  curfuncf  18188  curf2ndf  18197  yonffthlem  18232  acsfiindd  18503  sgrppropd  18619  mndpropd  18647  mhmeql  18704  smndex1mgm  18785  isgrpinv  18875  dfgrp3lem  18918  mhmmnd  18942  cycsubm  19074  cycsubmcom  19076  conjnmzb  19122  gass  19160  symgextf  19280  dfod2  19427  gexdvds  19447  sylow3lem2  19491  efgredlem  19610  efgredeu  19615  ghmcmn  19694  oddvdssubg  19718  dprdfcntz  19880  pgpfaclem3  19948  issrg  20005  isring  20054  dvdsrmul1  20176  issubdrg  20382  islmhm2  20642  lmhmeql  20659  lssacsex  20750  isphl  21173  uvcf1  21339  lindfmm  21374  sraassab  21414  issubassa2  21438  opsrval  21593  mhpmulcl  21684  scmatmats  22005  smatvscl  22018  mdetunilem7  22112  gsummatr01lem4  22152  m2cpmfo  22250  pmatcollpw3fi1lem1  22280  pm2mpf1lem  22288  pm2mpf1  22293  mp2pm2mplem4  22303  pm2mpghm  22310  chfacfscmulfsupp  22353  chfacfpmmulfsupp  22357  cctop  22501  neiptoptop  22627  neiptopreu  22629  tgrest  22655  ordtrest2lem  22699  cnss1  22772  cncnp  22776  isnrm3  22855  uncmp  22899  cmpfi  22904  iunconn  22924  1stcrest  22949  subislly  22977  islly2  22980  cldllycmp  22991  lly1stc  22992  llycmpkgen2  23046  kgencn  23052  xkoccn  23115  ptcnplem  23117  pthaus  23134  txhaus  23143  txkgen  23148  xkohaus  23149  xkococnlem  23155  txconn  23185  regr1lem2  23236  kqreglem1  23237  reghmph  23289  nrmhmph  23290  trfil2  23383  ufileu  23415  flimopn  23471  flimcf  23478  fclscf  23521  ufilcmp  23528  cnpfcf  23537  cnextfun  23560  tgpmulg  23589  symgtgp  23602  tgpt0  23615  qustgplem  23617  ustex2sym  23713  ustex3sym  23714  trust  23726  restutop  23734  restutopopn  23735  ustuqtop4  23741  utop3cls  23748  utopreg  23749  cstucnd  23781  ucncn  23782  trcfilu  23791  neipcfilu  23793  ismet2  23831  metequiv2  24011  metcnp  24042  metcnp2  24043  metcnpi3  24047  txmetcnp  24048  metustto  24054  metustsym  24056  metust  24059  cfilucfil  24060  metuel2  24066  psmetutop  24068  restmetu  24071  metucn  24072  ngptgp  24137  tngngp  24163  nmoleub  24240  icccmp  24333  reconnlem2  24335  reconn  24336  xmetdcn2  24345  metdseq0  24362  metdscn  24364  elcncf2  24398  cncfmet  24417  cnheibor  24463  nmoleub2lem2  24624  nmoleub3  24627  cvsi  24638  iscfil2  24775  iscfil3  24782  cfilfcls  24783  equivcfil  24808  caubl  24817  bcthlem5  24837  pmltpc  24959  ovollb2  24998  ovoliunnul  25016  ovolicc2lem4  25029  volsup  25065  ioorf  25082  dyadss  25103  dyaddisjlem  25104  mbfposr  25161  cncombf  25167  mbflimsup  25175  i1fmulclem  25212  mbfi1fseqlem4  25228  iblss2  25315  ellimc2  25386  ellimc3  25388  dvnadd  25438  dvmptfsum  25484  dvferm1  25494  dvferm2  25496  fta1g  25677  plyeq0lem  25716  plydivex  25802  fta1  25813  aalioulem2  25838  aalioulem3  25839  ulmuni  25896  ulmbdd  25902  ulmdvlem3  25906  mtest  25908  abelthlem8  25943  efopn  26158  cxpmul2z  26191  cxpcn3lem  26245  jensen  26483  lgambdd  26531  lgamucov  26532  isppw2  26609  mersenne  26720  dchrelbas3  26731  dchrptlem1  26757  dchrpt  26760  lgsval2lem  26800  lgsdchrval  26847  lgsquad3  26880  2sqb  26925  2sqmo  26930  pntrsumbnd2  27060  pntpbnd  27081  pntibnd  27086  nosupno  27196  noinfno  27211  noetasuplem4  27229  noetalem1  27234  madebday  27384  cofcutr  27401  negsprop  27499  mulscom  27585  tgjustr  27715  tglowdim1i  27742  tgbtwndiff  27747  tgifscgr  27749  iscgrglt  27755  tgcgrxfr  27759  lnext  27808  tgbtwnconn1lem3  27815  tgbtwnconn1  27816  legval  27825  legov  27826  legov2  27827  legtrd  27830  legtri3  27831  legso  27840  hlcgrex  27857  hlcgreu  27859  tglnne  27869  tglndim0  27870  tglineeltr  27872  tglinethru  27877  tglnne0  27881  tglnpt2  27882  colline  27890  tglowdim2l  27891  tglowdim2ln  27892  mirreu3  27895  miriso  27911  midexlem  27933  isperp  27953  perpcom  27954  perpneq  27955  isperp2  27956  footexALT  27959  footex  27962  colperpexlem3  27973  opphllem  27976  midex  27978  oppne3  27984  opptgdim2  27986  opphllem2  27989  opphllem3  27990  opphllem5  27992  opphllem6  27993  opphl  27995  outpasch  27996  lnopp2hpgb  28004  colopp  28010  lmieu  28025  trgcopy  28045  trgcopyeu  28047  iscgra1  28051  cgrane1  28053  cgrane2  28054  cgrane3  28055  cgrahl1  28057  cgrahl2  28058  cgracgr  28059  cgraswap  28061  cgracom  28063  cgratr  28064  flatcgra  28065  cgrabtwn  28067  cgrahl  28068  dfcgra2  28071  sacgr  28072  acopyeu  28075  inaghl  28086  cgrg3col4  28094  f1otrg  28112  f1otrge  28113  axsegcon  28175  axeuclidlem  28210  upgr1eopALT  28367  usgr1eop  28497  pthdepisspth  28982  wpthswwlks2on  29205  clwwlkf1  29292  clwwlknscsh  29305  2pthfrgr  29527  n4cyclfrgr  29534  frgrwopreglem5  29564  frgrwopreglem5ALT  29565  friendshipgt3  29641  smcnlem  29938  0lno  30031  ubthlem1  30111  ubthlem3  30113  chocunii  30542  occl  30545  5oalem1  30895  3oalem2  30904  nmopub2tALT  31150  nmfnleub2  31167  lnconi  31274  kbass5  31361  mdslmd1lem1  31566  mdslmd1lem2  31567  cdj1i  31674  opreu2reuALT  31705  disjabrex  31801  disjabrexf  31802  2ndresdju  31862  acunirnmpt  31872  acunirnmpt2  31873  acunirnmpt2f  31874  aciunf1lem  31875  fnpreimac  31884  fgreu  31885  suppovss  31894  xrge0infss  31961  xrofsup  31968  fsumiunle  32023  s3f1  32101  ccatf1  32103  swrdf1  32108  ressprs  32121  dfmgc2  32154  mgcf1o  32161  xrge0addgt0  32180  gsumle  32230  psgnfzto1stlem  32247  fzto1st1  32249  cycpmco2  32280  cycpmrn  32290  cyc3genpm  32299  cycpmconjs  32303  cyc3conja  32304  submarchi  32320  isarchi3  32321  archiabllem1  32327  archiabllem2a  32328  isdrng4  32384  suborng  32422  isarchiofld  32424  imaslmod  32457  dvdsruasso  32479  nsgqusf1olem2  32514  ghmquskerlem3  32520  ghmqusker  32521  lmhmqusker  32523  intlidl  32525  rhmpreimaidl  32526  rhmquskerlem  32532  elrspunidl  32535  elrspunsn  32536  rhmimaidl  32539  prmidl2  32548  isprmidlc  32555  rhmpreimaprmidl  32559  qsidomlem2  32561  mxidlprm  32575  ssmxidl  32579  opprqusplusg  32592  opprqusmulr  32594  qsdrngilem  32597  qsdrngi  32598  lindsunlem  32698  lindsun  32699  dimkerim  32701  fedgmullem1  32703  fedgmul  32705  minplyirred  32759  mdetpmtr1  32792  txomap  32803  qtophaus  32805  cmpcref  32819  zarclsun  32839  zarclssn  32842  zarcmplem  32850  pstmxmet  32866  sqsscirc1  32877  ordtrest2NEWlem  32891  ordtconnlem1  32893  pnfneige0  32920  lmxrge0  32921  lmdvg  32922  qqhval2  32951  esumcst  33050  esumrnmpt2  33055  esumfsup  33057  esumcvg  33073  esum2d  33080  esumiun  33081  sigaclfu2  33108  insiga  33124  ldsysgenld  33147  ldgenpisyslem1  33150  fiunelros  33161  measinb  33208  imambfm  33250  oms0  33285  omssubadd  33288  carsgclctunlem3  33308  eulerpartlemgvv  33364  dstrvprob  33459  sgnsub  33532  signstfvneq0  33572  actfunsnrndisj  33606  reprinfz1  33623  breprexp  33634  afsval  33672  derangenlem  34151  sconnpi1  34219  cvmsss2  34254  cvmopnlem  34258  cvmlift3lem7  34305  msrval  34518  ifscgr  35005  cgrxfr  35016  btwnconn1lem13  35060  outsideofeu  35092  neibastop2lem  35234  irrdifflemf  36195  irrdiff  36196  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem14  36491  poimirlem22  36499  poimirlem29  36506  broucube  36511  heicant  36512  mblfinlem1  36514  itg2addnclem  36528  ftc1cnnc  36549  ftc1anclem7  36556  sstotbnd2  36631  equivtotbnd  36635  isbnd3  36641  ssbnd  36645  totbndbnd  36646  cntotbnd  36653  heibor1lem  36666  rrncmslem  36689  lssats  37871  lsat0cv  37892  lkrlss  37954  lfl1dim  37980  lfl1dim2N  37981  lkrpssN  38022  hlhgt2  38249  3dim2  38328  2dim  38330  lplncvrlvol  38476  paddasslem11  38690  pmapjat1  38713  2polssN  38775  pclfinclN  38810  pexmidlem8N  38837  lhpexle1lem  38867  4atex  38936  ltrnid  38995  trlator0  39031  cdlemg2cex  39451  tendodi1  39644  tendodi2  39645  diblss  40030  dihopelvalcpre  40108  dihatexv  40198  mapdval4N  40492  fldhmf1  40944  aks6d1c2p2  40946  sticksstones8  40958  sticksstones12  40963  sticksstones22  40973  metakunt1  40974  metakunt2  40975  frlmsnic  41108  fsuppind  41160  sn-subeu  41296  sn-0tie0  41309  prjspersym  41346  dffltz  41373  nna4b4nsq  41399  mzpindd  41470  mzpsubst  41472  mzpcompact2lem  41475  eldioph2b  41487  irrapxlem3  41548  irrapxlem5  41550  pellex  41559  pell1234qrdich  41585  pell14qrexpcl  41591  congabseq  41699  jm2.26a  41725  jm2.26lem3  41726  rmydioph  41739  lnrfg  41847  hbt  41858  cantnftermord  42056  cantnfresb  42060  cantnf2  42061  oawordex2  42062  omabs2  42068  tfsconcatfv  42077  tfsconcatrev  42084  ofoaass  42096  nadd2rabtr  42120  nadd1suc  42128  naddgeoa  42131  rfovcnvf1od  42741  clsk3nimkb  42777  ntrneiiso  42828  ntrneikb  42831  ntrneixb  42832  ntrneik3  42833  ntrneix3  42834  ntrneik13  42835  ntrneix13  42836  4an4132  43246  iunconnlem2  43682  fnchoice  43699  cncmpmax  43702  ssinc  43762  ssdec  43763  disjf1  43866  supxrge  44035  suplesup  44036  infxr  44064  infleinf  44069  unb2ltle  44112  rexabslelem  44115  uzub  44128  supminfxr  44161  climrec  44306  climsuse  44311  islptre  44322  addlimc  44351  0ellimcdiv  44352  limsuppnfdlem  44404  limsupub  44407  limsuppnflem  44413  limsupubuz  44416  climinf3  44419  limsupmnflem  44423  climxrre  44453  liminfreuzlem  44505  liminflimsupclim  44510  xlimliminflimsup  44565  icccncfext  44590  cncfiooicclem1  44596  fperdvper  44622  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvmptfprodlem  44647  dvmptfprod  44648  dvnprodlem2  44650  stoweidlem7  44710  stoweidlem34  44737  stoweidlem52  44755  stoweidlem60  44763  wallispilem3  44770  fourierdlem34  44844  fourierdlem38  44848  fourierdlem39  44849  fourierdlem48  44857  fourierdlem50  44859  fourierdlem51  44860  fourierdlem73  44882  fourierdlem76  44885  fourierdlem77  44886  fourierdlem80  44889  fourierdlem87  44896  fourierdlem103  44912  fourierdlem104  44913  etransclem32  44969  etransclem33  44970  sge0f1o  45085  sge0pr  45097  sge0isum  45130  iundjiun  45163  meaiininclem  45189  pimdecfgtioo  45420  pimincfltioo  45421  preimageiingt  45423  preimaleiinlt  45424  smflimlem2  45475  smflimlem4  45477  smfmullem3  45496  smflimmpt  45513  smfinflem  45520  smfpimne2  45543  fsupdm  45545  finfdm  45549  cfsetsnfsetfo  45757  funressnbrafv2  45939  imasetpreimafvbijlemf1  46059  bgoldbtbndlem2  46461  bgoldbtbndlem3  46462  bgoldbtbnd  46464  isomuspgrlem2  46488  mgmhmeql  46560  isrng  46637  2zlidl  46786  lindslinindsimp2  47098  snlindsntor  47106  lincresunit2  47113  islindeps2  47118