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 398

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 209  df-an 399

This theorem is referenced by:  fsnex  7039  soisoi  7081  f1o2ndf1  7818  fimaproj  7829  tz7.49  8081  omabs  8274  omxpenlem  8618  fopwdom  8625  findcard3  8761  frfi  8763  finsschain  8831  marypha1lem  8897  wdomtr  9039  cantnfp1  9144  harcard  9407  numacn  9475  infunsdom1  9635  sornom  9699  ssfin4  9732  fin1a2lem11  9832  fin1a2lem13  9834  fpwwe2lem13  10064  pwfseq  10086  mulcmpblnr  10493  00id  10815  addid1  10820  cnegex  10821  negeu  10876  add20  11152  ltmul12a  11496  lediv12a  11533  fiminreOLD  11590  cru  11630  qextltlem  12596  xleadd1a  12647  xmullem  12658  xlemul1a  12682  ixxss12  12759  ioodisj  12869  fsuppmapnn0fz  13365  seqf1o  13412  mulexpz  13470  leexp1a  13540  faclbnd  13651  swrdswrdlem  14066  abs3lem  14698  rexico  14713  cau3lem  14714  rlim3  14855  ello12  14873  lo1bdd2  14881  elo12  14884  rlimconst  14901  isercoll  15024  climcau  15027  climbdd  15028  summolem2  15073  fsumconst  15145  o1fsum  15168  incexclem  15191  fprodconst  15332  bitsfzo  15784  dvdsmulgcd  15905  pc2dvds  16215  pcz  16217  pcadd  16225  pcfac  16235  vdwmc2  16315  vdwlem2  16318  vdwlem10  16326  vdw  16330  ramcl  16365  sbcie3s  16541  firest  16706  prdsval  16728  mreexd  16913  mreexexlemd  16915  iscat  16943  cidfval  16947  iscatd2  16952  catcocl  16956  catass  16957  catpropd  16979  cidpropd  16980  moni  17006  monpropd  17007  issubc  17105  subccocl  17115  funcco  17141  funcpropd  17170  fullpropd  17190  nati  17225  natpropd  17246  fucpropd  17247  xpcpropd  17458  curfuncf  17488  curf2ndf  17497  yonffthlem  17532  acsfiindd  17787  mndpropd  17936  mhmeql  17990  smndex1mgm  18072  isgrpinv  18156  dfgrp3lem  18197  mhmmnd  18221  cycsubm  18345  cycsubmcom  18347  conjnmzb  18393  gass  18431  symgextf  18545  dfod2  18691  gexdvds  18709  sylow3lem2  18753  efgredlem  18873  efgredeu  18878  ghmcmn  18952  oddvdssubg  18975  dprdfcntz  19137  pgpfaclem3  19205  issrg  19257  isring  19301  dvdsrmul1  19403  issubdrg  19560  islmhm2  19810  lmhmeql  19827  lssacsex  19916  issubassa2  20121  opsrval  20255  isphl  20772  uvcf1  20936  lindfmm  20971  scmatmats  21120  smatvscl  21133  mdetunilem7  21227  gsummatr01lem4  21267  m2cpmfo  21364  pmatcollpw3fi1lem1  21394  pm2mpf1lem  21402  pm2mpf1  21407  mp2pm2mplem4  21417  pm2mpghm  21424  chfacfscmulfsupp  21467  chfacfpmmulfsupp  21471  cctop  21614  neiptoptop  21739  neiptopreu  21741  tgrest  21767  ordtrest2lem  21811  cnss1  21884  cncnp  21888  isnrm3  21967  uncmp  22011  cmpfi  22016  iunconn  22036  1stcrest  22061  subislly  22089  islly2  22092  cldllycmp  22103  lly1stc  22104  llycmpkgen2  22158  kgencn  22164  xkoccn  22227  ptcnplem  22229  pthaus  22246  txhaus  22255  txkgen  22260  xkohaus  22261  xkococnlem  22267  txconn  22297  regr1lem2  22348  kqreglem1  22349  reghmph  22401  nrmhmph  22402  trfil2  22495  ufileu  22527  flimopn  22583  flimcf  22590  fclscf  22633  ufilcmp  22640  cnpfcf  22649  cnextfun  22672  tgpmulg  22701  symgtgp  22714  tgpt0  22727  qustgplem  22729  ustex2sym  22825  ustex3sym  22826  trust  22838  restutop  22846  restutopopn  22847  ustuqtop4  22853  utop3cls  22860  utopreg  22861  cstucnd  22893  ucncn  22894  trcfilu  22903  neipcfilu  22905  ismet2  22943  metequiv2  23120  metcnp  23151  metcnp2  23152  metcnpi3  23156  txmetcnp  23157  metustto  23163  metustsym  23165  metust  23168  cfilucfil  23169  metuel2  23175  psmetutop  23177  restmetu  23180  metucn  23181  ngptgp  23245  tngngp  23263  nmoleub  23340  icccmp  23433  reconnlem2  23435  reconn  23436  xmetdcn2  23445  metdseq0  23462  metdscn  23464  elcncf2  23498  cncfmet  23516  cnheibor  23559  nmoleub2lem2  23720  nmoleub3  23723  cvsi  23734  iscfil2  23869  iscfil3  23876  cfilfcls  23877  equivcfil  23902  caubl  23911  bcthlem5  23931  pmltpc  24051  ovollb2  24090  ovoliunnul  24108  ovolicc2lem4  24121  volsup  24157  ioorf  24174  dyadss  24195  dyaddisjlem  24196  mbfposr  24253  cncombf  24259  mbflimsup  24267  i1fmulclem  24303  mbfi1fseqlem4  24319  iblss2  24406  ellimc2  24475  ellimc3  24477  dvnadd  24526  dvmptfsum  24572  dvferm1  24582  dvferm2  24584  fta1g  24761  plyeq0lem  24800  plydivex  24886  fta1  24897  aalioulem2  24922  aalioulem3  24923  ulmuni  24980  ulmbdd  24986  ulmdvlem3  24990  mtest  24992  abelthlem8  25027  efopn  25241  cxpmul2z  25274  cxpcn3lem  25328  jensen  25566  lgambdd  25614  lgamucov  25615  isppw2  25692  mersenne  25803  dchrelbas3  25814  dchrptlem1  25840  dchrpt  25843  lgsval2lem  25883  lgsdchrval  25930  lgsquad3  25963  2sqb  26008  2sqmo  26013  pntrsumbnd2  26143  pntpbnd  26164  pntibnd  26169  istrkgc  26240  istrkgb  26241  tgjustr  26260  tglowdim1i  26287  tgbtwndiff  26292  tgifscgr  26294  iscgrglt  26300  tgcgrxfr  26304  lnext  26353  tgbtwnconn1lem3  26360  tgbtwnconn1  26361  legval  26370  legov  26371  legov2  26372  legtrd  26375  legtri3  26376  legso  26385  hlcgrex  26402  hlcgreu  26404  tglnne  26414  tglndim0  26415  tglineeltr  26417  tglinethru  26422  tglnne0  26426  tglnpt2  26427  colline  26435  tglowdim2l  26436  tglowdim2ln  26437  mirreu3  26440  miriso  26456  midexlem  26478  isperp  26498  perpcom  26499  perpneq  26500  isperp2  26501  footexALT  26504  footex  26507  colperpexlem3  26518  opphllem  26521  midex  26523  oppne3  26529  opptgdim2  26531  opphllem2  26534  opphllem3  26535  opphllem5  26537  opphllem6  26538  opphl  26540  outpasch  26541  lnopp2hpgb  26549  colopp  26555  lmieu  26570  trgcopy  26590  trgcopyeu  26592  iscgra1  26596  cgrane1  26598  cgrane2  26599  cgrane3  26600  cgrahl1  26602  cgrahl2  26603  cgracgr  26604  cgraswap  26606  cgracom  26608  cgratr  26609  flatcgra  26610  cgrabtwn  26612  cgrahl  26613  dfcgra2  26616  sacgr  26617  acopyeu  26620  inaghl  26631  cgrg3col4  26639  f1otrg  26657  f1otrge  26658  axsegcon  26713  axeuclidlem  26748  upgr1eopALT  26902  usgr1eop  27032  pthdepisspth  27516  wpthswwlks2on  27740  clwwlkf1  27828  clwwlknscsh  27841  2pthfrgr  28063  n4cyclfrgr  28070  frgrwopreglem5  28100  frgrwopreglem5ALT  28101  friendshipgt3  28177  smcnlem  28474  0lno  28567  ubthlem1  28647  ubthlem3  28649  chocunii  29078  occl  29081  5oalem1  29431  3oalem2  29440  nmopub2tALT  29686  nmfnleub2  29703  lnconi  29810  kbass5  29897  mdslmd1lem1  30102  mdslmd1lem2  30103  cdj1i  30210  opreu2reuALT  30240  disjabrex  30332  disjabrexf  30333  acunirnmpt  30404  acunirnmpt2  30405  acunirnmpt2f  30406  aciunf1lem  30407  fnpreimac  30416  fgreu  30417  suppovss  30426  xrge0infss  30484  xrofsup  30492  fsumiunle  30545  s3f1  30623  ccatf1  30625  swrdf1  30630  ressprs  30642  xrge0addgt0  30678  gsumle  30725  psgnfzto1stlem  30742  fzto1st1  30744  cycpmco2  30775  cycpmrn  30785  cyc3genpm  30794  cycpmconjs  30798  cyc3conja  30799  submarchi  30815  isarchi3  30816  archiabllem1  30822  archiabllem2a  30823  suborng  30888  isarchiofld  30890  imaslmod  30922  prmidl2  30958  isprmidlc  30963  qsidomlem2  30966  mxidlprm  30977  ssmxidl  30979  lindsunlem  31020  lindsun  31021  dimkerim  31023  fedgmullem1  31025  fedgmul  31027  mdetpmtr1  31088  txomap  31098  qtophaus  31100  cmpcref  31114  pstmxmet  31137  sqsscirc1  31151  ordtrest2NEWlem  31165  ordtconnlem1  31167  pnfneige0  31194  lmxrge0  31195  lmdvg  31196  qqhval2  31223  esumcst  31322  esumrnmpt2  31327  esumfsup  31329  esumcvg  31345  esum2d  31352  esumiun  31353  sigaclfu2  31380  insiga  31396  ldsysgenld  31419  ldgenpisyslem1  31422  fiunelros  31433  measinb  31480  imambfm  31520  oms0  31555  omssubadd  31558  carsgclctunlem3  31578  eulerpartlemgvv  31634  dstrvprob  31729  sgnsub  31802  signstfvneq0  31842  actfunsnrndisj  31876  reprinfz1  31893  breprexp  31904  afsval  31942  derangenlem  32418  sconnpi1  32486  cvmsss2  32521  cvmopnlem  32525  cvmlift3lem7  32572  msrval  32785  frpomin  33078  fprlem2  33138  frrlem16  33143  nosupno  33203  noetalem3  33219  noetalem5  33221  ifscgr  33505  cgrxfr  33516  btwnconn1lem13  33560  outsideofeu  33592  neibastop2lem  33708  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem14  34921  poimirlem22  34929  poimirlem29  34936  broucube  34941  heicant  34942  mblfinlem1  34944  itg2addnclem  34958  ftc1cnnc  34981  ftc1anclem7  34988  sstotbnd2  35067  equivtotbnd  35071  isbnd3  35077  ssbnd  35081  totbndbnd  35082  cntotbnd  35089  heibor1lem  35102  rrncmslem  35125  lssats  36163  lsat0cv  36184  lkrlss  36246  lfl1dim  36272  lfl1dim2N  36273  lkrpssN  36314  hlhgt2  36540  3dim2  36619  2dim  36621  lplncvrlvol  36767  paddasslem11  36981  pmapjat1  37004  2polssN  37066  pclfinclN  37101  pexmidlem8N  37128  lhpexle1lem  37158  4atex  37227  ltrnid  37286  trlator0  37322  cdlemg2cex  37742  tendodi1  37935  tendodi2  37936  diblss  38321  dihopelvalcpre  38399  dihatexv  38489  mapdval4N  38783  frlmsnic  39198  prjspersym  39306  dffltz  39320  mzpindd  39392  mzpsubst  39394  mzpcompact2lem  39397  eldioph2b  39409  irrapxlem3  39470  irrapxlem5  39472  pellex  39481  pell1234qrdich  39507  pell14qrexpcl  39513  congabseq  39620  jm2.26a  39646  jm2.26lem3  39647  rmydioph  39660  lnrfg  39768  hbt  39779  rfovcnvf1od  40399  clsk3nimkb  40439  ntrneiiso  40490  ntrneikb  40493  ntrneixb  40494  ntrneik3  40495  ntrneix3  40496  ntrneik13  40497  ntrneix13  40498  4an4132  40882  iunconnlem2  41318  fnchoice  41335  cncmpmax  41338  ssinc  41402  ssdec  41403  disjf1  41492  supxrge  41655  suplesup  41656  infxr  41684  infleinf  41689  unb2ltle  41738  rexabslelem  41741  uzub  41754  supminfxr  41789  climrec  41933  climsuse  41938  islptre  41949  addlimc  41978  0ellimcdiv  41979  limsuppnfdlem  42031  limsupub  42034  limsuppnflem  42040  limsupubuz  42043  climinf3  42046  limsupmnflem  42050  climxrre  42080  liminfreuzlem  42132  liminflimsupclim  42137  xlimliminflimsup  42192  icccncfext  42219  cncfiooicclem1  42225  fperdvper  42252  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvmptfprodlem  42278  dvmptfprod  42279  dvnprodlem2  42281  stoweidlem7  42341  stoweidlem34  42368  stoweidlem52  42386  stoweidlem60  42394  wallispilem3  42401  fourierdlem34  42475  fourierdlem38  42479  fourierdlem39  42480  fourierdlem48  42488  fourierdlem50  42490  fourierdlem51  42491  fourierdlem73  42513  fourierdlem76  42516  fourierdlem77  42517  fourierdlem80  42520  fourierdlem87  42527  fourierdlem103  42543  fourierdlem104  42544  etransclem32  42600  etransclem33  42601  sge0f1o  42713  sge0pr  42725  sge0isum  42758  iundjiun  42791  meaiininclem  42817  pimdecfgtioo  43044  pimincfltioo  43045  preimageiingt  43047  preimaleiinlt  43048  smflimlem2  43097  smflimlem4  43099  smfmullem3  43117  smflimmpt  43133  smfinflem  43140  funressnbrafv2  43492  imasetpreimafvbijlemf1  43613  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbnd  44023  isomuspgrlem2  44047  mgmhmeql  44119  isrng  44196  2zlidl  44254  lindslinindsimp2  44567  snlindsntor  44575  lincresunit2  44582  islindeps2  44587