Theorem simpllr 774

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  frpomin  6353  fsnex  7297  soisoi  7340  f1o2ndf1  8136  fimaproj  8149  fprlem2  8316  tz7.49  8475  omabs  8681  cofon1  8702  naddssim  8715  omxpenlem  9111  fopwdom  9118  findcard3  9319  findcard3OLD  9320  frfi  9322  finsschain  9403  marypha1lem  9476  wemappo  9592  wdomtr  9618  cantnfp1  9724  ttrcltr  9759  harcard  10021  numacn  10092  infunsdom1  10256  sornom  10320  ssfin4  10353  fin1a2lem11  10453  fin1a2lem13  10455  fpwwe2lem12  10685  pwfseq  10707  mulcmpblnr  11114  00id  11439  addrid  11444  cnegex  11445  negeu  11500  add20  11776  ltmul12a  12121  lediv12a  12159  cru  12256  qextltlem  13235  xleadd1a  13286  xmullem  13297  xlemul1a  13321  ixxss12  13398  ioodisj  13513  fsuppmapnn0fz  14016  seqf1o  14063  mulexpz  14122  leexp1a  14194  faclbnd  14307  swrdswrdlem  14712  abs3lem  15343  rexico  15358  cau3lem  15359  rlim3  15500  ello12  15518  lo1bdd2  15526  elo12  15529  rlimconst  15546  isercoll  15672  climcau  15675  climbdd  15676  summolem2  15720  fsumconst  15794  o1fsum  15817  incexclem  15840  fprodconst  15980  bitsfzo  16435  dvdsmulgcd  16557  pc2dvds  16881  pcz  16883  pcadd  16891  pcfac  16901  vdwmc2  16981  vdwlem2  16984  vdwlem10  16992  vdw  16996  ramcl  17031  sbcie3s  17164  firest  17447  prdsval  17470  mreexd  17655  mreexexlemd  17657  iscat  17685  cidfval  17689  iscatd2  17694  catcocl  17698  catass  17699  catpropd  17722  cidpropd  17723  moni  17752  monpropd  17753  issubc  17854  subccocl  17864  funcco  17890  funcpropd  17922  fullpropd  17942  nati  17978  natpropd  18001  fucpropd  18002  xpcpropd  18233  curfuncf  18263  curf2ndf  18272  yonffthlem  18307  acsfiindd  18578  mgmhmeql  18709  sgrppropd  18724  mndpropd  18752  mhmeql  18816  smndex1mgm  18897  isgrpinv  18988  dfgrp3lem  19032  mhmmnd  19058  cycsubm  19196  cycsubmcom  19198  conjnmzb  19247  ghmqusnsg  19276  ghmquskerlem3  19280  ghmqusker  19281  gass  19295  symgextf  19415  dfod2  19562  gexdvds  19582  sylow3lem2  19626  efgredlem  19745  efgredeu  19750  ghmcmn  19829  oddvdssubg  19853  dprdfcntz  20015  pgpfaclem3  20083  isrng  20137  issrg  20171  isring  20220  dvdsrmul1  20351  issubdrg  20759  islmhm2  21016  lmhmeql  21033  lssacsex  21125  rhmpreimaidl  21266  rhmqusnsg  21274  isphl  21624  uvcf1  21790  lindfmm  21825  sraassab  21865  issubassa2  21889  opsrval  22053  mhpmulcl  22143  psdmul  22160  scmatmats  22504  smatvscl  22517  mdetunilem7  22611  gsummatr01lem4  22651  m2cpmfo  22749  pmatcollpw3fi1lem1  22779  pm2mpf1lem  22787  pm2mpf1  22792  mp2pm2mplem4  22802  pm2mpghm  22809  chfacfscmulfsupp  22852  chfacfpmmulfsupp  22856  cctop  23000  neiptoptop  23126  neiptopreu  23128  tgrest  23154  ordtrest2lem  23198  cnss1  23271  cncnp  23275  isnrm3  23354  uncmp  23398  cmpfi  23403  iunconn  23423  1stcrest  23448  subislly  23476  islly2  23479  cldllycmp  23490  lly1stc  23491  llycmpkgen2  23545  kgencn  23551  xkoccn  23614  ptcnplem  23616  pthaus  23633  txhaus  23642  txkgen  23647  xkohaus  23648  xkococnlem  23654  txconn  23684  regr1lem2  23735  kqreglem1  23736  reghmph  23788  nrmhmph  23789  trfil2  23882  ufileu  23914  flimopn  23970  flimcf  23977  fclscf  24020  ufilcmp  24027  cnpfcf  24036  cnextfun  24059  tgpmulg  24088  symgtgp  24101  tgpt0  24114  qustgplem  24116  ustex2sym  24212  ustex3sym  24213  trust  24225  restutop  24233  restutopopn  24234  ustuqtop4  24240  utop3cls  24247  utopreg  24248  cstucnd  24280  ucncn  24281  trcfilu  24290  neipcfilu  24292  ismet2  24330  metequiv2  24510  metcnp  24541  metcnp2  24542  metcnpi3  24546  txmetcnp  24547  metustto  24553  metustsym  24555  metust  24558  cfilucfil  24559  metuel2  24565  psmetutop  24567  restmetu  24570  metucn  24571  ngptgp  24636  tngngp  24662  nmoleub  24739  icccmp  24832  reconnlem2  24834  reconn  24835  xmetdcn2  24844  metdseq0  24861  metdscn  24863  elcncf2  24901  cncfmet  24920  cnheibor  24972  nmoleub2lem2  25134  nmoleub3  25137  cvsi  25148  iscfil2  25285  iscfil3  25292  cfilfcls  25293  equivcfil  25318  caubl  25327  bcthlem5  25347  pmltpc  25470  ovollb2  25509  ovoliunnul  25527  ovolicc2lem4  25540  volsup  25576  ioorf  25593  dyadss  25614  dyaddisjlem  25615  mbfposr  25672  cncombf  25678  mbflimsup  25686  i1fmulclem  25723  mbfi1fseqlem4  25739  iblss2  25826  ellimc2  25897  ellimc3  25899  dvnadd  25950  dvmptfsum  25998  dvferm1  26008  dvferm2  26010  fta1g  26197  plyeq0lem  26237  plydivex  26325  fta1  26336  aalioulem2  26361  aalioulem3  26362  ulmuni  26421  ulmbdd  26427  ulmdvlem3  26431  mtest  26433  abelthlem8  26469  efopn  26685  cxpmul2z  26718  cxpcn3lem  26775  jensen  27017  lgambdd  27065  lgamucov  27066  isppw2  27143  mersenne  27256  dchrelbas3  27267  dchrptlem1  27293  dchrpt  27296  lgsval2lem  27336  lgsdchrval  27383  lgsquad3  27416  2sqb  27461  2sqmo  27466  pntrsumbnd2  27596  pntpbnd  27617  pntibnd  27622  nosupno  27733  noinfno  27748  noetasuplem4  27766  noetalem1  27771  madebday  27923  cofcutr  27941  negsprop  28044  mulscom  28140  absmuls  28239  remulscl  28353  tgjustr  28401  tglowdim1i  28428  tgbtwndiff  28433  tgifscgr  28435  iscgrglt  28441  tgcgrxfr  28445  lnext  28494  tgbtwnconn1lem3  28501  tgbtwnconn1  28502  legval  28511  legov  28512  legov2  28513  legtrd  28516  legtri3  28517  legso  28526  hlcgrex  28543  hlcgreu  28545  tglnne  28555  tglndim0  28556  tglineeltr  28558  tglinethru  28563  tglnne0  28567  tglnpt2  28568  colline  28576  tglowdim2l  28577  tglowdim2ln  28578  mirreu3  28581  miriso  28597  midexlem  28619  isperp  28639  perpcom  28640  perpneq  28641  isperp2  28642  footexALT  28645  footex  28648  colperpexlem3  28659  opphllem  28662  midex  28664  oppne3  28670  opptgdim2  28672  opphllem2  28675  opphllem3  28676  opphllem5  28678  opphllem6  28679  opphl  28681  outpasch  28682  lnopp2hpgb  28690  colopp  28696  lmieu  28711  trgcopy  28731  trgcopyeu  28733  iscgra1  28737  cgrane1  28739  cgrane2  28740  cgrane3  28741  cgrahl1  28743  cgrahl2  28744  cgracgr  28745  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  cgrabtwn  28753  cgrahl  28754  dfcgra2  28757  sacgr  28758  acopyeu  28761  inaghl  28772  cgrg3col4  28780  f1otrg  28798  f1otrge  28799  axsegcon  28861  axeuclidlem  28896  upgr1eopALT  29053  usgr1eop  29186  pthdepisspth  29672  wpthswwlks2on  29895  clwwlkf1  29982  clwwlknscsh  29995  2pthfrgr  30217  n4cyclfrgr  30224  frgrwopreglem5  30254  frgrwopreglem5ALT  30255  friendshipgt3  30331  smcnlem  30630  0lno  30723  ubthlem1  30803  ubthlem3  30805  chocunii  31234  occl  31237  5oalem1  31587  3oalem2  31596  nmopub2tALT  31842  nmfnleub2  31859  lnconi  31966  kbass5  32053  mdslmd1lem1  32258  mdslmd1lem2  32259  cdj1i  32366  opreu2reuALT  32405  disjabrex  32502  disjabrexf  32503  2ndresdju  32566  acunirnmpt  32576  acunirnmpt2  32577  acunirnmpt2f  32578  aciunf1lem  32579  fnpreimac  32588  fgreu  32589  suppovss  32597  xrge0infss  32664  xrofsup  32671  fsumiunle  32730  s3f1  32810  ccatf1  32812  ccatws1f1o  32815  swrdf1  32820  ressprs  32833  dfmgc2  32866  mgcf1o  32873  chnind  32880  chnso  32883  xrge0addgt0  32900  gsumle  32959  psgnfzto1stlem  32978  fzto1st1  32980  cycpmco2  33011  cycpmrn  33021  cyc3genpm  33030  cycpmconjs  33034  cyc3conja  33035  submarchi  33051  isarchi3  33052  archiabllem1  33058  archiabllem2a  33059  erler  33120  rlocaddval  33123  rlocmulval  33124  rloccring  33125  rloc1r  33127  subrdom  33137  isdrng4  33147  fracfld  33158  suborng  33193  isarchiofld  33195  imaslmod  33228  dvdsruasso  33260  unitprodclb  33264  nsgqusf1olem2  33289  lmhmqusker  33292  intlidl  33295  rhmquskerlem  33300  elrspunidl  33303  elrspunsn  33304  rhmimaidl  33307  prmidl2  33316  isprmidlc  33322  rhmpreimaprmidl  33326  qsidomlem2  33328  ssdifidllem  33331  ssdifidlprm  33333  mxidlprm  33345  ssmxidl  33349  opprqusplusg  33364  opprqusmulr  33366  qsdrngilem  33369  qsdrngi  33370  rsprprmprmidl  33397  rsprprmprmidlb  33398  rprmirred  33406  rprmirredb  33407  rprmdvdspow  33408  rprmdvdsprod  33409  1arithidom  33412  1arithufdlem2  33420  1arithufdlem3  33421  1arithufdlem4  33422  dfufd2lem  33424  dfufd2  33425  zringfrac  33429  ply1dg3rt0irred  33454  r1plmhm  33477  r1pquslmic  33478  lindsunlem  33519  lindsun  33520  dimkerim  33522  fedgmullem1  33524  fedgmul  33526  evls1fldgencl  33556  minplyirred  33580  constrmon  33602  constrconj  33603  fldext2chn  33606  mdetpmtr1  33638  txomap  33649  qtophaus  33651  cmpcref  33665  zarclsun  33685  zarclssn  33688  zarcmplem  33696  pstmxmet  33712  sqsscirc1  33723  ordtrest2NEWlem  33737  ordtconnlem1  33739  pnfneige0  33766  lmxrge0  33767  lmdvg  33768  qqhval2  33797  esumcst  33896  esumrnmpt2  33901  esumfsup  33903  esumcvg  33919  esum2d  33926  esumiun  33927  sigaclfu2  33954  insiga  33970  ldsysgenld  33993  ldgenpisyslem1  33996  fiunelros  34007  measinb  34054  imambfm  34096  oms0  34131  omssubadd  34134  carsgclctunlem3  34154  eulerpartlemgvv  34210  dstrvprob  34305  sgnsub  34378  signstfvneq0  34418  actfunsnrndisj  34451  reprinfz1  34468  breprexp  34479  afsval  34517  derangenlem  34999  sconnpi1  35067  cvmsss2  35102  cvmopnlem  35106  cvmlift3lem7  35153  msrval  35366  ifscgr  35868  cgrxfr  35879  btwnconn1lem13  35923  outsideofeu  35955  neibastop2lem  36072  irrdifflemf  37032  irrdiff  37033  matunitlindflem1  37317  matunitlindflem2  37318  poimirlem14  37335  poimirlem22  37343  poimirlem29  37350  broucube  37355  heicant  37356  mblfinlem1  37358  itg2addnclem  37372  ftc1cnnc  37393  ftc1anclem7  37400  sstotbnd2  37475  equivtotbnd  37479  isbnd3  37485  ssbnd  37489  totbndbnd  37490  cntotbnd  37497  heibor1lem  37510  rrncmslem  37533  lssats  38710  lsat0cv  38731  lkrlss  38793  lfl1dim  38819  lfl1dim2N  38820  lkrpssN  38861  hlhgt2  39088  3dim2  39167  2dim  39169  lplncvrlvol  39315  paddasslem11  39529  pmapjat1  39552  2polssN  39614  pclfinclN  39649  pexmidlem8N  39676  lhpexle1lem  39706  4atex  39775  ltrnid  39834  trlator0  39870  cdlemg2cex  40290  tendodi1  40483  tendodi2  40484  diblss  40869  dihopelvalcpre  40947  dihatexv  41037  mapdval4N  41331  fldhmf1  41789  mndmolinv  41793  primrootscoprmpow  41797  posbezout  41798  primrootscoprbij2  41801  primrootspoweq0  41804  aks6d1c2p2  41817  hashscontpow  41820  aks6d1c2lem4  41825  aks6d1c2  41828  aks6d1c5  41837  sticksstones8  41851  sticksstones12  41856  sticksstones22  41866  aks6d1c6lem3  41870  aks6d1c6isolem1  41872  metakunt1  41891  metakunt2  41892  frlmsnic  42012  fsuppind  42062  sn-subeu  42206  sn-0tie0  42219  prjspersym  42261  dffltz  42288  nna4b4nsq  42314  mzpindd  42403  mzpsubst  42405  mzpcompact2lem  42408  eldioph2b  42420  irrapxlem3  42481  irrapxlem5  42483  pellex  42492  pell1234qrdich  42518  pell14qrexpcl  42524  congabseq  42632  jm2.26a  42658  jm2.26lem3  42659  rmydioph  42672  lnrfg  42780  hbt  42791  cantnftermord  42986  cantnfresb  42990  cantnf2  42991  oawordex2  42992  omabs2  42998  tfsconcatfv  43007  tfsconcatrev  43014  ofoaass  43026  nadd2rabtr  43050  nadd1suc  43058  naddgeoa  43061  rfovcnvf1od  43671  clsk3nimkb  43707  ntrneiiso  43758  ntrneikb  43761  ntrneixb  43762  ntrneik3  43763  ntrneix3  43764  ntrneik13  43765  ntrneix13  43766  4an4132  44175  iunconnlem2  44611  fnchoice  44628  cncmpmax  44631  ssinc  44688  ssdec  44689  disjf1  44790  supxrge  44953  suplesup  44954  infxr  44982  infleinf  44987  unb2ltle  45030  rexabslelem  45033  uzub  45046  supminfxr  45079  climrec  45224  climsuse  45229  islptre  45240  addlimc  45269  0ellimcdiv  45270  limsuppnfdlem  45322  limsupub  45325  limsuppnflem  45331  limsupubuz  45334  climinf3  45337  limsupmnflem  45341  climxrre  45371  liminfreuzlem  45423  liminflimsupclim  45428  xlimliminflimsup  45483  icccncfext  45508  cncfiooicclem1  45514  fperdvper  45540  ioodvbdlimc1lem2  45553  ioodvbdlimc2lem  45555  dvmptfprodlem  45565  dvmptfprod  45566  dvnprodlem2  45568  stoweidlem7  45628  stoweidlem34  45655  stoweidlem52  45673  stoweidlem60  45681  wallispilem3  45688  fourierdlem34  45762  fourierdlem38  45766  fourierdlem39  45767  fourierdlem48  45775  fourierdlem50  45777  fourierdlem51  45778  fourierdlem73  45800  fourierdlem76  45803  fourierdlem77  45804  fourierdlem80  45807  fourierdlem87  45814  fourierdlem103  45830  fourierdlem104  45831  etransclem32  45887  etransclem33  45888  sge0f1o  46003  sge0pr  46015  sge0isum  46048  iundjiun  46081  meaiininclem  46107  pimdecfgtioo  46338  pimincfltioo  46339  preimageiingt  46341  preimaleiinlt  46342  smflimlem2  46393  smflimlem4  46395  smfmullem3  46414  smflimmpt  46431  smfinflem  46438  smfpimne2  46461  fsupdm  46463  finfdm  46467  cfsetsnfsetfo  46675  funressnbrafv2  46857  imasetpreimafvbijlemf1  46976  bgoldbtbndlem2  47378  bgoldbtbndlem3  47379  bgoldbtbnd  47381  isuspgrim  47454  2zlidl  47617  lindslinindsimp2  47846  snlindsntor  47854  lincresunit2  47861  islindeps2  47866