MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2 Unicode version

Theorem simp2 956
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )

Proof of Theorem simp2
StepHypRef Expression
1 3simpa 952 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simprd 449 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl2  959  simpr2  962  simp2i  965  simp2d  968  simp12  986  simp22  989  simp32  992  syld3an3  1227  disjss3  4038  nlim0  4466  reusv6OLD  4561  tfisi  4665  fresaun  5428  fvmptt  5631  fsnunf2  5735  fnsuppres  5748  fnfvima  5772  cocan1  5817  cocan2  5818  fveqf1o  5822  knatar  5873  ovmpt2x  5992  ovmpt2ga  5993  sorpssuni  6302  sorpssint  6303  onoviun  6376  smo11  6397  omeulem1  6596  oeord  6602  oecan  6603  domss2  7036  mapxpen  7043  mapdom3  7049  fofinf1o  7153  elfir  7185  ordtype2  7265  wemapso2  7283  wdomima2g  7316  ixpiunwdom  7321  oemapvali  7402  cnfcom3clem  7424  tcrank  7570  fodomfi2  7703  cdaassen  7824  xpcdaen  7825  mapcdaen  7826  infcdaabs  7848  infdif  7851  ackbij1lem16  7877  cfeq0  7898  cfsuc  7899  isfin2-2  7961  fin23lem26  7967  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  zornn0g  8148  ttukey2g  8159  canthwe  8289  gchhar  8309  gchaleph  8313  gchaleph2  8314  wunpw  8345  tsktrss  8399  tskcard  8419  tskwun  8422  tskxp  8425  tskmap  8426  tskurn  8427  gruixp  8447  enqeq  8574  ltadd2  8940  readdcan  9002  subadd2  9071  nppcan  9086  nppcan3  9087  subsub2  9091  subsub4  9096  npncan3  9101  pnpcan  9102  pnncan  9104  subcan  9118  ltadd1  9257  leadd1  9258  leadd2  9259  ltsubadd  9260  ltsubadd2  9261  lesubadd  9262  lesubadd2  9263  lesub1  9284  lesub2  9285  ltsub1  9286  ltsub2  9287  mulcan  9421  mulcan2  9422  divmul  9443  divcan1  9449  diveq0  9450  divrec  9456  divass  9458  div23  9459  divdir  9463  divcan3  9464  div11  9466  diveq1  9470  divmuldiv  9476  divcan5  9478  redivcl  9495  div2neg  9499  ltmul1  9622  ltdiv1  9636  ledivmulOLD  9646  ledivmul2OLD  9650  lemuldiv  9651  lt2msq1  9655  ltdiv23  9663  lediv23  9664  infmrlb  9751  ofsubeq0  9759  ofnegsub  9760  ofsubge0  9761  zsupss  10323  suprzub  10325  rpgecl  10395  xrmaxlt  10526  xrltmin  10527  xrmaxle  10528  xrlemin  10529  xleadd1  10591  xltadd1  10592  xlemul1  10626  xlemul2  10627  xltmul1  10628  xadddir  10632  supxrre  10662  infmxrre  10670  ixxub  10693  icc0  10720  ubioc1  10721  ubicc2  10769  icoshftf1o  10775  snunioo  10778  snunico  10779  iccsplit  10784  fzm1  10878  flwordi  10958  flword2  10959  modcyc  11015  axdc4uzlem  11060  expgt1  11156  exprec  11159  expmulz  11164  leexp2a  11173  expubnd  11178  bernneq2  11244  expmulnbnd  11249  digit2  11250  swrdval  11466  ccatco  11506  s3cl  11543  swrds2  11576  shftuz  11580  cjdiv  11665  resqrcl  11755  absdiv  11796  caubnd  11858  limsuple  11968  limsuplt  11969  climuni  12042  iseraltlem3  12172  geoisum1c  12352  eflt  12413  dvdsval2  12550  dvdsadd2b  12587  dvdsexp  12600  dvdsgcdb  12739  mulgcd  12741  gcddiv  12744  mulgcddvds  12799  qredeq  12801  rpexp12i  12817  fermltl  12868  prmdiv  12869  odzcllem  12873  odzphi  12877  coprimeprodsq  12878  pythagtriplem6  12890  pythagtriplem7  12891  pythagtriplem13  12896  pceu  12915  pcgcd1  12945  vdwpc  13043  hashbcss  13067  ramval  13071  0ram2  13084  0ramcl  13086  isstruct2  13173  ressbas  13214  imasvscaval  13456  xpsadd  13494  xpsmul  13495  mrerintcl  13515  ismred2  13521  mremre  13522  mrieqv2d  13557  mreexmrid  13561  cofuass  13779  cofulid  13780  cofurid  13781  catcisolem  13954  posasymb  14102  ple1  14166  latleeqj1  14185  latleeqm1  14201  latnlemlt  14206  ipodrsfi  14282  mrelatglb  14303  mrelatlub  14305  imasmnd2  14425  imasmnd  14426  pwspjmhm  14460  frmdss2  14501  frmdup3  14504  grpinvadd  14560  grpsubeq0  14568  grppncan  14572  grpsubpropd2  14583  mulgnn0p1  14594  mulgnnsubcl  14595  mulgnn0subcl  14596  mulgsubcl  14597  mulgneg  14601  submmulg  14618  pwsinvg  14623  imasgrp2  14626  imasgrp  14627  subgcl  14647  subgsubcl  14648  subgsub  14649  subgmulg  14651  nsgconj  14666  cycsubg2cl  14671  nsgid  14679  ghmmulg  14711  ghmeqker  14725  odcong  14880  oddvds2  14895  odsubdvds  14898  pgpssslw  14941  slwn0  14942  sylow2blem1  14947  lsmssv  14970  lsmsubm  14980  lsmsubg  14981  subglsm  14998  lsmpropd  15002  pj1fval  15019  efgsval2  15058  frgp0  15085  frgpup3  15103  ablinvadd  15127  ablsub4  15130  ablpncan2  15133  subgabl  15148  cntzcmn  15152  gex2abl  15159  lsmsubg2  15167  prdscmnd  15169  ablfacrp  15317  rngidss  15383  rngcom  15385  gsumdixp  15408  imasrng  15418  unitmulcl  15462  unitmulclb  15463  dvrcan1  15489  dvrcan3  15490  irredrmul  15505  subrgmcl  15573  subrgdv  15578  cntzsubr  15593  isabvd  15601  islmod  15647  lmodvsnegOLD  15684  lmodcom  15687  lssvnegcl  15729  lssintcl  15737  lspss  15757  lspun  15760  lspsnvsi  15777  lmodvsinv  15809  lmodvsinv2  15810  0lmhm  15813  lmhmvsca  15818  reslmhm2  15826  lbsind2  15850  lsmsp  15855  lspsntri  15866  lsmcv  15910  lvecdim  15926  lbsextlem2  15928  lbsextg  15931  rrgeq0  16047  domneq0  16054  domnrrg  16057  aspss  16088  asclmul1  16095  asclmul2  16096  psrbagaddcl  16132  psrbagconcl  16135  psrgrp  16159  psrlmod  16162  psrrng  16171  psrcrng  16173  evlslem4  16261  psrplusgpropd  16329  psropprmul  16332  coe1add  16357  coe1mul2  16362  ply1tmcl  16364  coe1tm  16365  coe1tmfv1  16366  coe1sclmul  16374  coe1sclmul2  16376  chrcong  16499  zndvds  16519  ipeq0  16558  ip2eq  16573  cssmre  16609  obselocv  16644  clsndisj  16828  iscldtop  16848  lpss3  16892  restabs  16912  restcldi  16920  restlp  16929  mnfnei  16967  lmconst  17007  cnrest2  17030  cnpresti  17032  hausnei2  17097  sshauslem  17116  cmpcld  17145  fiuncmp  17147  hauscmp  17150  concompclo  17177  2ndc1stc  17193  nllyrest  17228  kgen2ss  17266  xkopjcn  17366  xkococn  17370  cnmpt2t  17383  elqtop  17404  r0cld  17445  cmphaushmeo  17507  filss  17564  isfild  17569  fbasweak  17576  snfbas  17577  trfg  17602  trnei  17603  supfil  17606  ufinffr  17640  ufilen  17641  flimrest  17694  flimclslem  17695  lmflf  17716  fclsneii  17728  fclsrest  17735  cnpfcfi  17751  ptcmpg  17767  istgp2  17790  tgpconcompeqg  17810  prdstmdd  17822  tsmsxp  17853  xmetge0  17925  xmetsym  17928  blval  17964  xblcntr  17979  xmssym  18027  blsscls2  18066  stdbdxmet  18077  prdsxms  18092  prdsms  18093  isngp4  18149  nmmtri  18159  nmsub  18160  nmrtri  18161  nmtri  18163  nlmmul0or  18210  nmods  18269  xrsmopn  18334  iccntr  18342  metds0  18370  cncfmptc  18431  iirev  18443  icoopnst  18453  iocopnst  18454  icchmeo  18455  iccpnfhmeo  18459  pi1grplem  18563  pi1xfr  18569  isclmi  18591  cphreccllem  18630  ipcau  18684  nmpar  18686  fmcfil  18714  iscau2  18719  cfilres  18738  caussi  18739  caublcls  18750  bcthlem5  18766  srabn  18793  rlmbn  18794  pjth  18819  pjth2  18820  cniccbdd  18837  ovolgelb  18855  ovollecl  18858  ovolunnul  18875  ovolicc  18898  cmmbl  18908  iundisj2  18922  voliunlem2  18924  voliunlem3  18925  ovolioo  18941  volcn  18977  cncombf  19029  itg1le  19084  itg2lecl  19109  itgconst  19189  bddibl  19210  dvfval  19263  dvid  19283  dvcnp  19284  dvcnp2  19285  dvnf  19292  dvnbss  19293  dvn2bss  19295  evlsval2  19420  mdegldg  19468  deg1lt  19499  deg1mul3  19517  deg1mul3le  19518  q1peqb  19556  r1pcl  19559  r1pdeglt  19560  r1pid  19561  dvdsr1p  19563  fta1b  19571  drnguc1p  19572  ig1peu  19573  elplyr  19599  dgrub  19632  dgrlb  19634  dgradd2  19665  ofmulrt  19678  quotcl2  19698  quotdgr  19699  quotcan  19705  vieta1  19708  aannenlem1  19724  aannenlem2  19725  aalioulem3  19730  aaliou2  19736  ulmcl  19776  tanord1  19915  tanord  19916  cxpef  20028  cxpadd  20042  cxpneg  20044  cxpsub  20045  divcxp  20050  cxpmul  20051  cxpeq  20113  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  angpieqvd  20144  xrlimcnp  20279  cxp2lim  20287  wilthlem3  20324  chtwordi  20410  ppiwordi  20416  sgmppw  20452  dchrabl  20509  bcmono  20532  efexple  20536  lgsneg1  20575  lgsmod  20576  lgssq  20590  lgsdirnn0  20594  lgsdinn0  20595  lgsqrlem5  20600  lgsquad  20612  dirith  20694  pntrmax  20729  abvcxp  20780  grpoasscan2  20921  grpoinvop  20924  grpopncan  20934  grponpcan  20935  gxcom  20952  gxinv  20953  gxsuc  20955  gxdi  20979  rngodi  21068  rngosn  21087  nvpncan2  21230  nvnncan  21237  nvs  21244  nvdif  21247  nvpi  21248  nvabs  21255  nv1  21258  lno0  21350  lnocoi  21351  nmooge0  21361  shlub  22009  pjspansn  22172  adj2  22530  kbmul  22551  adjlnop  22682  cdj3lem3a  23035  xreceu  23121  xdivcl  23123  xdivmul  23124  xdivrec  23126  curry2ima  23262  snunioc  23282  iocinioc2  23287  cnre2csqlem  23309  xrsmulgzz  23322  xrge0addass  23344  xrge0neqmnf  23345  xrge0adddir  23347  iundisj2fi  23379  iundisj2f  23381  relogbcl  23419  logb1  23420  logblt  23423  esummulc1  23464  hasheuni  23468  sigaclcu  23493  difelsiga  23509  elsigagen2  23524  isrnmeas  23546  measvun  23552  measxun2  23553  measvunilem  23555  measvunilem0  23556  measvuni  23557  measres  23564  mbfmco2  23585  ind1  23617  probun  23637  totprob  23645  probmeasb  23648  cndprobval  23651  cndprobtot  23654  cndprobnul  23655  cndprobprob  23656  bayesth  23657  orvclteinc  23691  cvmcov2  23821  dedekind  24097  dedekindle  24098  subdivcomb2  24106  faclimlem5  24121  trpredpo  24309  elno2  24379  brbtwn2  24605  colinearalglem1  24606  colinearalglem2  24607  axcgrid  24616  ax5seglem2  24629  axbtwnid  24639  axpasch  24641  axcontlem4  24667  axcontlem8  24671  cgrrflx  24682  cgrtriv  24697  btwntriv2  24707  btwntriv1  24711  trisegint  24723  btwnxfr  24751  colineardim1  24756  colineartriv1  24762  colineartriv2  24763  btwnconn1lem7  24788  segcon2  24800  seglerflx  24807  outsidene2  24819  liness  24840  hilbert1.1  24849  bpolycl  24859  areacirclem4  25030  areacirclem6  25033  areacirc  25034  intn3an2d  25040  infxpg  25198  iccleub2  25238  injsurinj  25252  iscst2  25278  mop  25288  preotr2  25338  altprs2  25339  supdefa  25366  inposet  25381  reacomsmgrp1  25446  reacomsmgrp3  25448  reacomsmgrp4  25449  isppm  25457  mndoass  25462  fprodneg  25481  multinv  25525  multinvb  25526  fldax4  25534  zerdivemp1  25539  mvecrtol2  25580  islp3  25617  mapdiscn  25630  hmeogrpi  25639  istopxc  25651  conttnf2  25665  islimrs3  25684  islimrs4  25685  mslb1  25710  2wsms  25711  msra3  25712  iintlem1  25713  limnumrr  25725  flfneic  25727  lvsovso2  25730  issubrv  25775  ismulcv  25784  distsava  25792  isdivcv2  25796  divclcvd  25797  divclrvd  25798  cmpassoh  25904  imonclem  25916  ismonc  25917  tartarmap  25991  indcls2  26099  elhalop2  26172  isconcl6a  26206  isibg1a2  26220  isibg2a2  26223  isibg1a6  26228  segline  26244  pxysxy  26245  lppotos  26247  rayline  26259  pdiveql  26271  comppfsc  26410  mettrifi  26576  cnresima  26587  ismtybndlem  26633  rrnmval  26655  zerdivemp1x  26689  isfldidl  26796  ismrcd1  26876  istopclsd  26878  ismrc  26879  mapfzcons  26896  mzpcl34  26912  mzpexpmpt  26926  mzpsubst  26929  eldioph  26940  diophrw  26941  pellexlem5  27021  pellex  27023  pell14qrgap  27063  pellfundlb  27072  pellfundglb  27073  pellfundex  27074  rmxycomplete  27105  rmxyadd  27109  monotoddzz  27131  rmxypos  27137  rmygeid  27154  acongrep  27170  acongeq  27173  coprmdvdsb  27177  modabsdifz  27181  dvdsabsmod0  27182  jm2.22  27191  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  rpnnen3lem  27227  pwssplit0  27290  pwssplit1  27291  pwssplit2  27292  pwssplit3  27293  pwssplit4  27294  dsmmsubg  27312  uvcresum  27345  frlmsplit2  27346  frlmsslss  27347  frlmup4  27356  isnumbasgrplem2  27372  islindf2  27387  lindfind2  27391  hbtlem2  27431  mpaaeu  27458  pmtrmvd  27501  pmtrfrn  27503  pmtrfb  27509  psgnunilem4  27523  matrng  27583  idomrootle  27614  fiuneneq  27616  proot1hash  27622  ofdivrec  27646  ofdivcan4  27647  ubelsupr  27794  fnchoice  27803  refsumcn  27804  fmul01  27813  fmuldfeq  27816  fmul01lt1lem2  27818  fmul01lt1  27819  climsuse  27837  ibliccsinexp  27848  stoweidlem3  27855  stoweidlem6  27858  stoweidlem8  27860  stoweidlem10  27862  stoweidlem17  27869  stoweidlem19  27871  stoweidlem22  27874  stoweidlem26  27878  stoweidlem28  27880  stoweidlem31  27883  stoweidlem34  27886  stoweidlem43  27895  stoweidlem46  27898  stoweidlem48  27900  stoweidlem49  27901  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  stoweidlem55  27907  stoweidlem56  27908  stoweidlem57  27909  stoweidlem58  27910  stoweidlem59  27911  stoweidlem60  27912  stoweid  27915  wallispilem3  27919  stirlinglem13  27938  sigaraf  27946  sigarmf  27947  sigaras  27948  sigarms  27949  sigarls  27950  sigarexp  27952  sigarperm  27953  sigarcol  27957  cusgra3v  28299  3orbi123  28572  alrim3con13v  28595  3orbi123VD  28942  19.21a3con13vVD  28944  tratrbVD  28953  bnj906  29278  bnj1110  29328  bnj1128  29336  bnj1145  29339  bnj1189  29355  bnj1204  29358  bnj1279  29364  bnj1311  29370  bnj1408  29382  toycom  29784  lshpnelb  29796  lsatfixedN  29821  lssatomic  29823  lcvat  29842  lsatcveq0  29844  lcvexchlem4  29849  lcvexchlem5  29850  lsatcvatlem  29861  islshpcv  29865  l1cvpat  29866  lfladd  29878  lflsub  29879  lflmul  29880  lfl1  29882  eqlkr  29911  lkrshp  29917  lshpsmreu  29921  lshpkrex  29930  ldualgrplem  29957  lduallmodlem  29964  lkrlspeqN  29983  oldmm1  30029  olj01  30037  omllaw4  30058  omllaw5N  30059  cmt2N  30062  cmt3N  30063  cmtbr2N  30065  cmtbr3N  30066  cmtbr4N  30067  lecmtN  30068  meetat  30108  atn0  30120  cvlcvr1  30151  cvlcvrp  30152  cvlsupr6  30159  hlrelat2  30214  exatleN  30215  cvr2N  30222  hlrelat3  30223  cvrval3  30224  cvrval4N  30225  cvrval5  30226  cvrexch  30231  lnnat  30238  atle  30247  atlt  30248  2atlt  30250  atbtwnexOLDN  30258  atbtwnex  30259  1cvratlt  30285  ps-2b  30293  3atlem5  30298  llnnleat  30324  llnle  30329  llnexatN  30332  llncmp  30333  2llnmat  30335  lplni2  30348  lvolex3N  30349  lplnle  30351  lplnnleat  30353  lplncmp  30373  lplnexatN  30374  2atnelvolN  30398  4atlem10  30417  4atlem11  30420  4atlem12  30423  lvolcmp  30428  dalemswapyz  30467  dalemswapyzps  30501  dalem56  30539  pmaple  30572  lneq2at  30589  lnjatN  30591  lncmp  30594  2lnat  30595  elpadd2at  30617  pmapjat1  30664  pmapjat2  30665  dalawlem10  30691  dalawlem13  30694  dalawlem15  30696  dalaw  30697  elpcliN  30704  pclunN  30709  polcon3N  30728  paddunN  30738  poldmj1N  30739  pmapj2N  30740  osumcllem5N  30771  osumcllem7N  30773  osumcllem10N  30776  lhp0lt  30814  lhpexle1  30819  lhpexle2lem  30820  lhpexle3lem  30822  lhpj1  30833  lhpmcvr5N  30838  lhpat4N  30855  4atexlem7  30886  4atex3  30892  ldilcnv  30926  ldilco  30927  ltrnatb  30948  ltrnel  30950  ltrncnvel  30953  ltrn11at  30958  ltrnmw  30962  trlval2  30974  trljat2  30978  trlat  30980  trl0  30981  trlnidat  30984  trlnidatb  30988  trlval3  30998  cdlemc1  31002  cdlemc2  31003  cdlemd8  31016  cdlemd9  31017  cdleme0ex2N  31035  cdleme7b  31055  cdleme7d  31057  cdleme10  31065  cdleme11dN  31073  cdleme11e  31074  cdleme21h  31145  cdleme26ee  31171  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdlemefs29bpre0N  31227  cdlemefs29bpre1N  31228  cdlemefs29cpre1N  31229  cdlemefs29clN  31230  cdlemefs32fvaN  31233  cdlemefs32fva1  31234  cdleme32fva  31248  cdleme32fvaw  31250  cdleme32le  31258  cdleme38m  31274  cdleme39a  31276  cdleme17d3  31307  cdlemeg49le  31322  cdlemeg46fvaw  31327  cdlemf1  31372  cdlemfnid  31375  cdlemg2ce  31403  cdlemb3  31417  cdlemg7fvbwN  31418  cdlemg4b1  31420  cdlemg7aN  31436  cdlemg10bALTN  31447  cdlemg12b  31455  cdlemg12d  31457  cdlemg12f  31459  cdlemg12g  31460  cdlemg13  31463  cdlemg31c  31510  cdlemg34  31523  cdlemg36  31525  trlcone  31539  cdlemg44  31544  cdlemg48  31548  tendococl  31583  tendoicl  31607  tendocan  31635  cdlemk7  31659  cdlemk12  31661  cdlemk12u  31683  cdlemk26b-3  31716  cdlemk26-3  31717  cdlemk11ta  31740  cdlemk19ylem  31741  cdlemkid3N  31744  cdlemk11tc  31756  cdlemk11t  31757  cdlemk45  31758  cdlemk46  31759  cdlemk49  31762  cdlemk54  31769  cdlemk55b  31771  cdlemk56  31782  cdlemk19w  31783  cdleml3N  31789  cdleml4N  31790  cdleml6  31792  cdleml7  31793  cdleml8  31794  erngdvlem4-rN  31810  tendocnv  31833  tendospcanN  31835  dia2dimlem12  31887  tendoinvcl  31916  tendolinv  31917  tendorinv  31918  dvhopellsm  31929  dicvaddcl  32002  dicvscacl  32003  cdlemn3  32009  cdlemn4  32010  cdlemn4a  32011  dihord2cN  32033  dihord11c  32036  dih1dimb2  32053  dihvalcq2  32059  dihord5b  32071  dihord5apre  32074  dihglblem2N  32106  dihjatc1  32123  dihmeetlem20N  32138  dihmeetALTN  32139  dih1dimatlem0  32140  dihatexv  32150  dochss  32177  dochdmj1  32202  dvh4dimlem  32255  dvh3dim3N  32261  dochsatshpb  32264  dochexmidlem4  32275  dochexmidlem5  32276  dochexmidlem8  32279  dochkr1  32290  dochkr1OLDN  32291  lcfl7lem  32311  lcfl8  32314  lcfrlem16  32370  lcfrlem40  32394  mapdval2N  32442  mapdpglem24  32516  mapdh6iN  32556  mapdh8ad  32591  mapdh8e  32596  hdmap1fval  32609  hdmap1l6i  32631  hdmapfval  32642  hdmapval0  32648  hdmapevec  32650  hdmapval3N  32653  hdmap10lem  32654  hdmap11lem2  32657  hdmaprnlem15N  32676  hdmaprnlem16N  32677  hdmap14lem10  32692  hdmap14lem11  32693  hdmap14lem12  32694  hgmapfval  32701  hgmapval1  32708  hgmapadd  32709  hgmapmul  32710  hgmaprnlem3N  32713  hgmaprnlem4N  32714  hgmap11  32717  hlhilsrnglem  32768  hlhilphllem  32774
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator