Theorem simpllr 776

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  frpomin  6172  fsnex  7071  soisoi  7115  f1o2ndf1  7869  fimaproj  7880  fprlem2  8020  tz7.49  8159  omabs  8354  omxpenlem  8724  fopwdom  8731  findcard3  8892  frfi  8894  finsschain  8961  marypha1lem  9027  wemappo  9143  wdomtr  9169  cantnfp1  9274  harcard  9559  numacn  9628  infunsdom1  9792  sornom  9856  ssfin4  9889  fin1a2lem11  9989  fin1a2lem13  9991  fpwwe2lem12  10221  pwfseq  10243  mulcmpblnr  10650  00id  10972  addid1  10977  cnegex  10978  negeu  11033  add20  11309  ltmul12a  11653  lediv12a  11690  cru  11787  qextltlem  12757  xleadd1a  12808  xmullem  12819  xlemul1a  12843  ixxss12  12920  ioodisj  13035  fsuppmapnn0fz  13534  seqf1o  13582  mulexpz  13640  leexp1a  13710  faclbnd  13821  swrdswrdlem  14234  abs3lem  14867  rexico  14882  cau3lem  14883  rlim3  15024  ello12  15042  lo1bdd2  15050  elo12  15053  rlimconst  15070  isercoll  15196  climcau  15199  climbdd  15200  summolem2  15245  fsumconst  15317  o1fsum  15340  incexclem  15363  fprodconst  15503  bitsfzo  15957  dvdsmulgcd  16080  pc2dvds  16395  pcz  16397  pcadd  16405  pcfac  16415  vdwmc2  16495  vdwlem2  16498  vdwlem10  16506  vdw  16510  ramcl  16545  sbcie3s  16722  firest  16891  prdsval  16914  mreexd  17099  mreexexlemd  17101  iscat  17129  cidfval  17133  iscatd2  17138  catcocl  17142  catass  17143  catpropd  17166  cidpropd  17167  moni  17195  monpropd  17196  issubc  17295  subccocl  17305  funcco  17331  funcpropd  17361  fullpropd  17381  nati  17416  natpropd  17439  fucpropd  17440  xpcpropd  17670  curfuncf  17700  curf2ndf  17709  yonffthlem  17744  acsfiindd  18013  mndpropd  18152  mhmeql  18206  smndex1mgm  18288  isgrpinv  18374  dfgrp3lem  18415  mhmmnd  18439  cycsubm  18563  cycsubmcom  18565  conjnmzb  18611  gass  18649  symgextf  18763  dfod2  18909  gexdvds  18927  sylow3lem2  18971  efgredlem  19091  efgredeu  19096  ghmcmn  19171  oddvdssubg  19194  dprdfcntz  19356  pgpfaclem3  19424  issrg  19476  isring  19520  dvdsrmul1  19625  issubdrg  19779  islmhm2  20029  lmhmeql  20046  lssacsex  20135  isphl  20544  uvcf1  20708  lindfmm  20743  issubassa2  20806  opsrval  20957  mhpmulcl  21043  scmatmats  21362  smatvscl  21375  mdetunilem7  21469  gsummatr01lem4  21509  m2cpmfo  21607  pmatcollpw3fi1lem1  21637  pm2mpf1lem  21645  pm2mpf1  21650  mp2pm2mplem4  21660  pm2mpghm  21667  chfacfscmulfsupp  21710  chfacfpmmulfsupp  21714  cctop  21857  neiptoptop  21982  neiptopreu  21984  tgrest  22010  ordtrest2lem  22054  cnss1  22127  cncnp  22131  isnrm3  22210  uncmp  22254  cmpfi  22259  iunconn  22279  1stcrest  22304  subislly  22332  islly2  22335  cldllycmp  22346  lly1stc  22347  llycmpkgen2  22401  kgencn  22407  xkoccn  22470  ptcnplem  22472  pthaus  22489  txhaus  22498  txkgen  22503  xkohaus  22504  xkococnlem  22510  txconn  22540  regr1lem2  22591  kqreglem1  22592  reghmph  22644  nrmhmph  22645  trfil2  22738  ufileu  22770  flimopn  22826  flimcf  22833  fclscf  22876  ufilcmp  22883  cnpfcf  22892  cnextfun  22915  tgpmulg  22944  symgtgp  22957  tgpt0  22970  qustgplem  22972  ustex2sym  23068  ustex3sym  23069  trust  23081  restutop  23089  restutopopn  23090  ustuqtop4  23096  utop3cls  23103  utopreg  23104  cstucnd  23135  ucncn  23136  trcfilu  23145  neipcfilu  23147  ismet2  23185  metequiv2  23362  metcnp  23393  metcnp2  23394  metcnpi3  23398  txmetcnp  23399  metustto  23405  metustsym  23407  metust  23410  cfilucfil  23411  metuel2  23417  psmetutop  23419  restmetu  23422  metucn  23423  ngptgp  23488  tngngp  23506  nmoleub  23583  icccmp  23676  reconnlem2  23678  reconn  23679  xmetdcn2  23688  metdseq0  23705  metdscn  23707  elcncf2  23741  cncfmet  23760  cnheibor  23806  nmoleub2lem2  23967  nmoleub3  23970  cvsi  23981  iscfil2  24117  iscfil3  24124  cfilfcls  24125  equivcfil  24150  caubl  24159  bcthlem5  24179  pmltpc  24301  ovollb2  24340  ovoliunnul  24358  ovolicc2lem4  24371  volsup  24407  ioorf  24424  dyadss  24445  dyaddisjlem  24446  mbfposr  24503  cncombf  24509  mbflimsup  24517  i1fmulclem  24554  mbfi1fseqlem4  24570  iblss2  24657  ellimc2  24728  ellimc3  24730  dvnadd  24780  dvmptfsum  24826  dvferm1  24836  dvferm2  24838  fta1g  25019  plyeq0lem  25058  plydivex  25144  fta1  25155  aalioulem2  25180  aalioulem3  25181  ulmuni  25238  ulmbdd  25244  ulmdvlem3  25248  mtest  25250  abelthlem8  25285  efopn  25500  cxpmul2z  25533  cxpcn3lem  25587  jensen  25825  lgambdd  25873  lgamucov  25874  isppw2  25951  mersenne  26062  dchrelbas3  26073  dchrptlem1  26099  dchrpt  26102  lgsval2lem  26142  lgsdchrval  26189  lgsquad3  26222  2sqb  26267  2sqmo  26272  pntrsumbnd2  26402  pntpbnd  26423  pntibnd  26428  istrkgc  26499  istrkgb  26500  tgjustr  26519  tglowdim1i  26546  tgbtwndiff  26551  tgifscgr  26553  iscgrglt  26559  tgcgrxfr  26563  lnext  26612  tgbtwnconn1lem3  26619  tgbtwnconn1  26620  legval  26629  legov  26630  legov2  26631  legtrd  26634  legtri3  26635  legso  26644  hlcgrex  26661  hlcgreu  26663  tglnne  26673  tglndim0  26674  tglineeltr  26676  tglinethru  26681  tglnne0  26685  tglnpt2  26686  colline  26694  tglowdim2l  26695  tglowdim2ln  26696  mirreu3  26699  miriso  26715  midexlem  26737  isperp  26757  perpcom  26758  perpneq  26759  isperp2  26760  footexALT  26763  footex  26766  colperpexlem3  26777  opphllem  26780  midex  26782  oppne3  26788  opptgdim2  26790  opphllem2  26793  opphllem3  26794  opphllem5  26796  opphllem6  26797  opphl  26799  outpasch  26800  lnopp2hpgb  26808  colopp  26814  lmieu  26829  trgcopy  26849  trgcopyeu  26851  iscgra1  26855  cgrane1  26857  cgrane2  26858  cgrane3  26859  cgrahl1  26861  cgrahl2  26862  cgracgr  26863  cgraswap  26865  cgracom  26867  cgratr  26868  flatcgra  26869  cgrabtwn  26871  cgrahl  26872  dfcgra2  26875  sacgr  26876  acopyeu  26879  inaghl  26890  cgrg3col4  26898  f1otrg  26916  f1otrge  26917  axsegcon  26972  axeuclidlem  27007  upgr1eopALT  27162  usgr1eop  27292  pthdepisspth  27776  wpthswwlks2on  27999  clwwlkf1  28086  clwwlknscsh  28099  2pthfrgr  28321  n4cyclfrgr  28328  frgrwopreglem5  28358  frgrwopreglem5ALT  28359  friendshipgt3  28435  smcnlem  28732  0lno  28825  ubthlem1  28905  ubthlem3  28907  chocunii  29336  occl  29339  5oalem1  29689  3oalem2  29698  nmopub2tALT  29944  nmfnleub2  29961  lnconi  30068  kbass5  30155  mdslmd1lem1  30360  mdslmd1lem2  30361  cdj1i  30468  opreu2reuALT  30498  disjabrex  30594  disjabrexf  30595  2ndresdju  30659  acunirnmpt  30670  acunirnmpt2  30671  acunirnmpt2f  30672  aciunf1lem  30673  fnpreimac  30682  fgreu  30683  suppovss  30691  xrge0infss  30757  xrofsup  30764  fsumiunle  30817  s3f1  30895  ccatf1  30897  swrdf1  30902  ressprs  30914  dfmgc2  30947  mgcf1o  30954  xrge0addgt0  30973  gsumle  31023  psgnfzto1stlem  31040  fzto1st1  31042  cycpmco2  31073  cycpmrn  31083  cyc3genpm  31092  cycpmconjs  31096  cyc3conja  31097  submarchi  31113  isarchi3  31114  archiabllem1  31120  archiabllem2a  31121  suborng  31187  isarchiofld  31189  imaslmod  31221  nsgqusf1olem2  31267  intlidl  31270  rhmpreimaidl  31271  elrspunidl  31274  rhmimaidl  31277  prmidl2  31284  isprmidlc  31291  rhmpreimaprmidl  31295  qsidomlem2  31297  mxidlprm  31308  ssmxidl  31310  lindsunlem  31373  lindsun  31374  dimkerim  31376  fedgmullem1  31378  fedgmul  31380  mdetpmtr1  31441  txomap  31452  qtophaus  31454  cmpcref  31468  zarclsun  31488  zarclssn  31491  zarcmplem  31499  pstmxmet  31515  sqsscirc1  31526  ordtrest2NEWlem  31540  ordtconnlem1  31542  pnfneige0  31569  lmxrge0  31570  lmdvg  31571  qqhval2  31598  esumcst  31697  esumrnmpt2  31702  esumfsup  31704  esumcvg  31720  esum2d  31727  esumiun  31728  sigaclfu2  31755  insiga  31771  ldsysgenld  31794  ldgenpisyslem1  31797  fiunelros  31808  measinb  31855  imambfm  31895  oms0  31930  omssubadd  31933  carsgclctunlem3  31953  eulerpartlemgvv  32009  dstrvprob  32104  sgnsub  32177  signstfvneq0  32217  actfunsnrndisj  32251  reprinfz1  32268  breprexp  32279  afsval  32317  derangenlem  32800  sconnpi1  32868  cvmsss2  32903  cvmopnlem  32907  cvmlift3lem7  32954  msrval  33167  frrlem16  33506  naddssim  33523  nosupno  33592  noinfno  33607  noetasuplem4  33625  noetalem1  33630  madebday  33766  cofcutr  33778  ifscgr  34032  cgrxfr  34043  btwnconn1lem13  34087  outsideofeu  34119  neibastop2lem  34235  irrdifflemf  35179  irrdiff  35180  matunitlindflem1  35459  matunitlindflem2  35460  poimirlem14  35477  poimirlem22  35485  poimirlem29  35492  broucube  35497  heicant  35498  mblfinlem1  35500  itg2addnclem  35514  ftc1cnnc  35535  ftc1anclem7  35542  sstotbnd2  35618  equivtotbnd  35622  isbnd3  35628  ssbnd  35632  totbndbnd  35633  cntotbnd  35640  heibor1lem  35653  rrncmslem  35676  lssats  36712  lsat0cv  36733  lkrlss  36795  lfl1dim  36821  lfl1dim2N  36822  lkrpssN  36863  hlhgt2  37089  3dim2  37168  2dim  37170  lplncvrlvol  37316  paddasslem11  37530  pmapjat1  37553  2polssN  37615  pclfinclN  37650  pexmidlem8N  37677  lhpexle1lem  37707  4atex  37776  ltrnid  37835  trlator0  37871  cdlemg2cex  38291  tendodi1  38484  tendodi2  38485  diblss  38870  dihopelvalcpre  38948  dihatexv  39038  mapdval4N  39332  sticksstones8  39778  sticksstones12  39783  metakunt1  39788  metakunt2  39789  frlmsnic  39916  fsuppind  39930  sn-subeu  40057  sn-0tie0  40070  prjspersym  40095  dffltz  40115  nna4b4nsq  40141  mzpindd  40212  mzpsubst  40214  mzpcompact2lem  40217  eldioph2b  40229  irrapxlem3  40290  irrapxlem5  40292  pellex  40301  pell1234qrdich  40327  pell14qrexpcl  40333  congabseq  40440  jm2.26a  40466  jm2.26lem3  40467  rmydioph  40480  lnrfg  40588  hbt  40599  rfovcnvf1od  41230  clsk3nimkb  41268  ntrneiiso  41319  ntrneikb  41322  ntrneixb  41323  ntrneik3  41324  ntrneix3  41325  ntrneik13  41326  ntrneix13  41327  4an4132  41733  iunconnlem2  42169  fnchoice  42186  cncmpmax  42189  ssinc  42251  ssdec  42252  disjf1  42334  supxrge  42491  suplesup  42492  infxr  42520  infleinf  42525  unb2ltle  42569  rexabslelem  42572  uzub  42585  supminfxr  42620  climrec  42762  climsuse  42767  islptre  42778  addlimc  42807  0ellimcdiv  42808  limsuppnfdlem  42860  limsupub  42863  limsuppnflem  42869  limsupubuz  42872  climinf3  42875  limsupmnflem  42879  climxrre  42909  liminfreuzlem  42961  liminflimsupclim  42966  xlimliminflimsup  43021  icccncfext  43046  cncfiooicclem1  43052  fperdvper  43078  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvmptfprodlem  43103  dvmptfprod  43104  dvnprodlem2  43106  stoweidlem7  43166  stoweidlem34  43193  stoweidlem52  43211  stoweidlem60  43219  wallispilem3  43226  fourierdlem34  43300  fourierdlem38  43304  fourierdlem39  43305  fourierdlem48  43313  fourierdlem50  43315  fourierdlem51  43316  fourierdlem73  43338  fourierdlem76  43341  fourierdlem77  43342  fourierdlem80  43345  fourierdlem87  43352  fourierdlem103  43368  fourierdlem104  43369  etransclem32  43425  etransclem33  43426  sge0f1o  43538  sge0pr  43550  sge0isum  43583  iundjiun  43616  meaiininclem  43642  pimdecfgtioo  43869  pimincfltioo  43870  preimageiingt  43872  preimaleiinlt  43873  smflimlem2  43922  smflimlem4  43924  smfmullem3  43942  smflimmpt  43958  smfinflem  43965  cfsetsnfsetfo  44169  funressnbrafv2  44351  imasetpreimafvbijlemf1  44472  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  bgoldbtbnd  44877  isomuspgrlem2  44901  mgmhmeql  44973  isrng  45050  2zlidl  45108  lindslinindsimp2  45420  snlindsntor  45428  lincresunit2  45435  islindeps2  45440