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

Theorem simp2 958
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 954 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simprd 450 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl2  961  simpr2  964  simp2i  967  simp2d  970  simp12  988  simp22  991  simp32  994  syld3an3  1229  intn3an2d  1294  disjss3  4203  nlim0  4631  reusv6OLD  4726  tfisi  4830  feq123  5576  fresaun  5606  fvmptt  5812  fsnunf2  5924  fnsuppres  5944  fnfvima  5968  cocan1  6016  cocan2  6017  fveqf1o  6021  knatar  6072  ovmpt2x  6194  ovmpt2ga  6195  sorpssuni  6523  sorpssint  6524  onoviun  6597  smo11  6618  omeulem1  6817  oeord  6823  oecan  6824  domss2  7258  mapxpen  7265  mapdom3  7271  fofinf1o  7379  elfir  7412  ordtype2  7495  wemapso2  7513  wdomima2g  7546  ixpiunwdom  7551  oemapvali  7632  cnfcom3clem  7654  tcrank  7800  fodomfi2  7933  cdaassen  8054  xpcdaen  8055  mapcdaen  8056  infcdaabs  8078  infdif  8081  ackbij1lem16  8107  cfeq0  8128  cfsuc  8129  isfin2-2  8191  fin23lem26  8197  domtriomlem  8314  axdc3lem2  8323  axdc3lem4  8325  axdc4lem  8327  zornn0g  8377  ttukey2g  8388  canthwe  8518  gchhar  8538  gchaleph  8542  gchaleph2  8543  wunpw  8574  tsktrss  8628  tskcard  8648  tskwun  8651  tskxp  8654  tskmap  8655  tskurn  8656  gruixp  8676  enqeq  8803  ltadd2  9169  readdcan  9232  subadd2  9301  nppcan  9316  nppcan3  9317  subsub2  9321  subsub4  9326  npncan3  9331  pnpcan  9332  pnncan  9334  subcan  9348  ltadd1  9487  leadd1  9488  leadd2  9489  ltsubadd  9490  ltsubadd2  9491  lesubadd  9492  lesubadd2  9493  lesub1  9514  lesub2  9515  ltsub1  9516  ltsub2  9517  mulcan  9651  mulcan2  9652  divmul  9673  divcan1  9679  diveq0  9680  divrec  9686  divass  9688  div23  9689  divdir  9693  divcan3  9694  div11  9696  diveq1  9700  divmuldiv  9706  divcan5  9708  redivcl  9725  div2neg  9729  ltmul1  9852  ltdiv1  9866  ledivmulOLD  9876  ledivmul2OLD  9880  lemuldiv  9881  lt2msq1  9885  ltdiv23  9893  lediv23  9894  infmrlb  9981  ofsubeq0  9989  ofnegsub  9990  ofsubge0  9991  zsupss  10557  suprzub  10559  rpgecl  10629  xrmaxlt  10761  xrltmin  10762  xrmaxle  10763  xrlemin  10764  xleadd1  10826  xltadd1  10827  xlemul1  10861  xlemul2  10862  xltmul1  10863  xadddir  10867  supxrre  10898  infmxrre  10906  ixxub  10929  icc0  10956  ubioc1  10957  ubicc2  11006  icoshftf1o  11012  snunioo  11015  snunico  11016  iccsplit  11021  fzm1  11119  flwordi  11211  flword2  11212  modcyc  11268  axdc4uzlem  11313  expgt1  11410  exprec  11413  expmulz  11418  leexp2a  11427  expubnd  11432  bernneq2  11498  expmulnbnd  11503  digit2  11504  swrdval  11756  ccatco  11796  s3cl  11833  swrds2  11872  shftuz  11876  cjdiv  11961  resqrcl  12051  absdiv  12092  caubnd  12154  limsuple  12264  limsuplt  12265  climuni  12338  iseraltlem3  12469  geoisum1c  12649  eflt  12710  dvdsval2  12847  dvdsadd2b  12884  dvdsexp  12897  dvdsgcdb  13036  mulgcd  13038  gcddiv  13041  mulgcddvds  13096  qredeq  13098  rpexp12i  13114  fermltl  13165  prmdiv  13166  odzcllem  13170  odzphi  13174  coprimeprodsq  13175  pythagtriplem6  13187  pythagtriplem7  13188  pythagtriplem13  13193  pceu  13212  pcgcd1  13242  vdwpc  13340  hashbcss  13364  ramval  13368  0ram2  13381  0ramcl  13383  isstruct2  13470  ressbas  13511  imasvscaval  13755  xpsadd  13793  xpsmul  13794  mrerintcl  13814  ismred2  13820  mremre  13821  mrieqv2d  13856  mreexmrid  13860  cofuass  14078  cofulid  14079  cofurid  14080  catcisolem  14253  posasymb  14401  ple1  14465  latleeqj1  14484  latleeqm1  14500  latnlemlt  14505  ipodrsfi  14581  mrelatglb  14602  mrelatlub  14604  imasmnd2  14724  imasmnd  14725  pwspjmhm  14759  frmdss2  14800  frmdup3  14803  grpinvadd  14859  grpsubeq0  14867  grppncan  14871  grpsubpropd2  14882  mulgnn0p1  14893  mulgnnsubcl  14894  mulgnn0subcl  14895  mulgsubcl  14896  mulgneg  14900  submmulg  14917  pwsinvg  14922  imasgrp2  14925  imasgrp  14926  subgcl  14946  subgsubcl  14947  subgsub  14948  subgmulg  14950  nsgconj  14965  cycsubg2cl  14970  nsgid  14978  ghmmulg  15010  ghmeqker  15024  odcong  15179  oddvds2  15194  odsubdvds  15197  pgpssslw  15240  slwn0  15241  sylow2blem1  15246  lsmssv  15269  lsmsubm  15279  lsmsubg  15280  subglsm  15297  lsmpropd  15301  pj1fval  15318  efgsval2  15357  frgp0  15384  frgpup3  15402  ablinvadd  15426  ablsub4  15429  ablpncan2  15432  subgabl  15447  cntzcmn  15451  gex2abl  15458  lsmsubg2  15466  prdscmnd  15468  ablfacrp  15616  rngidss  15682  rngcom  15684  gsumdixp  15707  imasrng  15717  unitmulcl  15761  unitmulclb  15762  dvrcan1  15788  dvrcan3  15789  irredrmul  15804  subrgmcl  15872  subrgdv  15877  cntzsubr  15892  isabvd  15900  islmod  15946  lmodcom  15982  lssvnegcl  16024  lssintcl  16032  lspss  16052  lspun  16055  lspsnvsi  16072  lmodvsinv  16104  lmodvsinv2  16105  0lmhm  16108  lmhmvsca  16113  reslmhm2  16121  lbsind2  16145  lsmsp  16150  lspsntri  16161  lsmcv  16205  lvecdim  16221  lbsextlem2  16223  lbsextg  16226  rrgeq0  16342  domneq0  16349  domnrrg  16352  aspss  16383  asclmul1  16390  asclmul2  16391  psrbagaddcl  16427  psrbagconcl  16430  psrgrp  16454  psrlmod  16457  psrrng  16466  psrcrng  16468  evlslem4  16556  psrplusgpropd  16621  psropprmul  16624  coe1add  16649  coe1mul2  16654  ply1tmcl  16656  coe1tm  16657  coe1tmfv1  16658  coe1sclmul  16666  coe1sclmul2  16668  chrcong  16802  zndvds  16822  ipeq0  16861  ip2eq  16876  cssmre  16912  obselocv  16947  clsndisj  17131  iscldtop  17151  lpss3  17200  islp3  17202  restabs  17221  restcldi  17229  neitr  17236  restlp  17239  mnfnei  17277  lmconst  17317  cnrest2  17342  cnpresti  17344  hausnei2  17409  sshauslem  17428  cmpcld  17457  fiuncmp  17459  hauscmp  17462  concompclo  17490  2ndc1stc  17506  nllyrest  17541  kgen2ss  17579  xkopjcn  17680  xkococn  17684  cnmpt2t  17697  elqtop  17721  r0cld  17762  cmphaushmeo  17824  filss  17877  isfild  17882  fbasweak  17889  snfbas  17890  trfg  17915  trnei  17916  supfil  17919  ufinffr  17953  ufilen  17954  flimrest  18007  flimclslem  18008  lmflf  18029  fclsneii  18041  fclsrest  18048  cnpfcfi  18064  ptcmpg  18080  istgp2  18113  tgpconcompeqg  18133  prdstmdd  18145  tsmsxp  18176  ustssel  18227  ustn0  18242  ressusp  18287  cfiluweak  18317  neipcfilu  18318  psmetsym  18333  psmetge0  18335  xmetge0  18366  xmetsym  18369  blvalps  18407  blval  18408  xblcntrps  18432  xblcntr  18433  xmssym  18487  blsscls2  18526  stdbdxmet  18537  prdsxms  18552  prdsms  18553  metustblOLD  18602  metustbl  18603  restmetu  18609  isngp4  18650  nmmtri  18660  nmsub  18661  nmrtri  18662  nmtri  18664  nlmmul0or  18711  nmods  18770  xrsmopn  18835  iccntr  18844  metds0  18872  cncfmptc  18933  iirev  18946  icoopnst  18956  iocopnst  18957  icchmeo  18958  iccpnfhmeo  18962  pi1grplem  19066  pi1xfr  19072  isclmi  19094  cphreccllem  19133  ipcau  19187  nmpar  19189  fmcfil  19217  iscau2  19222  cfilres  19241  caussi  19242  caublcls  19253  bcthlem5  19273  srabn  19306  rlmbn  19307  pjth  19332  pjth2  19333  cniccbdd  19350  ovolgelb  19368  ovollecl  19371  ovolunnul  19388  ovolicc  19411  cmmbl  19421  iundisj2  19435  voliunlem2  19437  voliunlem3  19438  ovolioo  19454  volcn  19490  cncombf  19542  itg1le  19597  itg2lecl  19622  itgconst  19702  bddibl  19723  dvfval  19776  dvid  19796  dvcnp  19797  dvcnp2  19798  dvnf  19805  dvnbss  19806  dvn2bss  19808  evlsval2  19933  mdegldg  19981  deg1lt  20012  deg1mul3  20030  deg1mul3le  20031  q1peqb  20069  r1pcl  20072  r1pdeglt  20073  r1pid  20074  dvdsr1p  20076  fta1b  20084  drnguc1p  20085  ig1peu  20086  elplyr  20112  dgrub  20145  dgrlb  20147  dgradd2  20178  ofmulrt  20191  quotcl2  20211  quotdgr  20212  quotcan  20218  vieta1  20221  aannenlem1  20237  aannenlem2  20238  aalioulem3  20243  aaliou2  20249  ulmcl  20289  tanord1  20431  tanord  20432  cxpef  20548  cxpadd  20562  cxpneg  20564  cxpsub  20565  divcxp  20570  cxpmul  20571  cxpeq  20633  ang180lem1  20643  ang180lem2  20644  ang180lem3  20645  ang180lem4  20646  angpieqvd  20664  xrlimcnp  20799  cxp2lim  20807  wilthlem3  20845  chtwordi  20931  ppiwordi  20937  sgmppw  20973  dchrabl  21030  bcmono  21053  efexple  21057  lgsneg1  21096  lgsmod  21097  lgssq  21111  lgsdirnn0  21115  lgsdinn0  21116  lgsqrlem5  21121  lgsquad  21133  dirith  21215  pntrmax  21250  abvcxp  21301  cusgra3v  21465  2trllemE  21545  1pthon  21583  2pthon  21594  grpoasscan2  21818  grpoinvop  21821  grpopncan  21831  grponpcan  21832  gxcom  21849  gxinv  21850  gxsuc  21852  gxdi  21876  rngodi  21965  rngosn  21984  zerdivemp1  22014  nvpncan2  22129  nvnncan  22136  nvs  22143  nvdif  22146  nvpi  22147  nvabs  22154  nv1  22157  lno0  22249  lnocoi  22250  nmooge0  22260  shlub  22908  pjspansn  23071  adj2  23429  kbmul  23450  adjlnop  23581  cdj3lem3a  23934  iundisj2f  24022  curry2ima  24089  snunioc  24129  iocinioc2  24134  iundisj2fi  24145  divnumden2  24153  xreceu  24160  xdivcl  24162  xdivmul  24163  xdivrec  24165  ress0g  24174  tleile  24181  xrsmulgzz  24192  xrge0addass  24203  xrge0neqmnf  24204  cnre2csqlem  24300  nmmulg  24344  qqhval2lem  24357  relogbcl  24394  logb1  24395  logblt  24398  ind1  24408  esummulc1  24463  hasheuni  24467  sigaclcu  24492  difelsiga  24508  elsigagen2  24523  sigagenss2  24525  isrnmeas  24546  measvun  24555  measvunilem  24558  measvunilem0  24559  measvuni  24560  measres  24568  aean  24587  mbfmco2  24607  dya2icoseg2  24620  sitgclg  24648  totprob  24677  probmeasb  24680  cndprobval  24683  cndprobnul  24687  cndprobprob  24688  bayesth  24689  orvclteinc  24725  lgamgulmlem1  24805  cvmcov2  24954  dedekind  25179  dedekindle  25180  subdivcomb2  25188  binomrisefac  25350  predeq123  25432  trpredpo  25505  wsuceq123  25557  wzel  25567  elno2  25601  brbtwn2  25836  colinearalglem1  25837  colinearalglem2  25838  axcgrid  25847  ax5seglem2  25860  axbtwnid  25870  axpasch  25872  axcontlem4  25898  axcontlem8  25902  cgrrflx  25913  cgrtriv  25928  btwntriv2  25938  btwntriv1  25942  trisegint  25954  btwnxfr  25982  colineardim1  25987  colineartriv1  25993  colineartriv2  25994  btwnconn1lem7  26019  segcon2  26031  seglerflx  26038  outsidene2  26050  liness  26071  hilbert1.1  26080  bpolycl  26090  areacirclem4  26284  areacirclem6  26287  areacirc  26288  comppfsc  26378  mettrifi  26454  cnresima  26464  ismtybndlem  26506  rrnmval  26528  zerdivemp1x  26562  isfldidl  26669  ismrcd1  26743  istopclsd  26745  ismrc  26746  mapfzcons  26763  mzpcl34  26779  mzpexpmpt  26793  mzpsubst  26796  eldioph  26807  diophrw  26808  pellexlem5  26887  pellex  26889  pell14qrgap  26929  pellfundlb  26938  pellfundglb  26939  pellfundex  26940  rmxycomplete  26971  rmxyadd  26975  monotoddzz  26997  rmxypos  27003  rmygeid  27020  acongrep  27036  acongeq  27039  coprmdvdsb  27043  modabsdifz  27047  dvdsabsmod0  27048  jm2.22  27057  rmydioph  27076  rmxdioph  27078  expdiophlem2  27084  rpnnen3lem  27093  pwssplit0  27155  pwssplit1  27156  pwssplit2  27157  pwssplit3  27158  pwssplit4  27159  dsmmsubg  27177  uvcresum  27210  frlmsplit2  27211  frlmsslss  27212  frlmup4  27221  isnumbasgrplem2  27237  islindf2  27252  lindfind2  27256  hbtlem2  27296  mpaaeu  27323  pmtrmvd  27366  pmtrfrn  27368  pmtrfb  27374  psgnunilem4  27388  matrng  27448  idomrootle  27479  fiuneneq  27481  proot1hash  27487  ofdivrec  27511  ofdivcan4  27512  ubelsupr  27658  fmul01  27677  fmuldfeq  27680  fmul01lt1lem2  27682  fmul01lt1  27683  climsuse  27701  stoweidlem3  27719  stoweidlem6  27722  stoweidlem8  27724  stoweidlem10  27726  stoweidlem19  27735  stoweidlem26  27742  stoweidlem28  27744  stoweidlem31  27747  stoweidlem57  27773  stoweidlem59  27775  stoweidlem60  27776  wallispilem3  27783  stirlinglem13  27802  sigaraf  27810  sigarmf  27811  sigaras  27812  sigarms  27813  sigarls  27814  sigarexp  27816  sigarperm  27817  sigarcol  27821  ssfzo12  28113  ltdifltdiv  28126  modsubmod  28133  modsubmodmod  28134  ccatsymb  28152  swrd0swrd  28163  cshwidxm1  28211  2cshw2lem2  28219  3cshw  28232  usgra2wlkspth  28261  el2wlkonotot0  28292  vdn0frgrav2  28351  vdn1frgrav2  28353  3orbi123  28531  alrim3con13v  28554  3orbi123VD  28899  19.21a3con13vVD  28901  tratrbVD  28910  bnj906  29238  bnj1110  29288  bnj1128  29296  bnj1145  29299  bnj1189  29315  bnj1204  29318  bnj1279  29324  bnj1311  29330  bnj1408  29342  toycom  29707  lshpnelb  29719  lsatfixedN  29744  lssatomic  29746  lcvat  29765  lsatcveq0  29767  lcvexchlem4  29772  lcvexchlem5  29773  lsatcvatlem  29784  islshpcv  29788  l1cvpat  29789  lfladd  29801  lflsub  29802  lflmul  29803  lfl1  29805  eqlkr  29834  lkrshp  29840  lshpsmreu  29844  lshpkrex  29853  ldualgrplem  29880  lduallmodlem  29887  lkrlspeqN  29906  oldmm1  29952  olj01  29960  omllaw4  29981  omllaw5N  29982  cmt2N  29985  cmt3N  29986  cmtbr2N  29988  cmtbr3N  29989  cmtbr4N  29990  lecmtN  29991  meetat  30031  atn0  30043  cvlcvr1  30074  cvlcvrp  30075  cvlsupr6  30082  hlrelat2  30137  exatleN  30138  cvr2N  30145  hlrelat3  30146  cvrval3  30147  cvrval4N  30148  cvrval5  30149  cvrexch  30154  lnnat  30161  atle  30170  atlt  30171  2atlt  30173  atbtwnexOLDN  30181  atbtwnex  30182  1cvratlt  30208  ps-2b  30216  3atlem5  30221  llnnleat  30247  llnle  30252  llnexatN  30255  llncmp  30256  2llnmat  30258  lplni2  30271  lvolex3N  30272  lplnle  30274  lplnnleat  30276  lplncmp  30296  lplnexatN  30297  2atnelvolN  30321  4atlem10  30340  4atlem11  30343  4atlem12  30346  lvolcmp  30351  dalemswapyz  30390  dalemswapyzps  30424  dalem56  30462  pmaple  30495  lneq2at  30512  lnjatN  30514  lncmp  30517  2lnat  30518  elpadd2at  30540  pmapjat1  30587  pmapjat2  30588  dalawlem10  30614  dalawlem13  30617  dalawlem15  30619  dalaw  30620  elpcliN  30627  pclunN  30632  polcon3N  30651  paddunN  30661  poldmj1N  30662  pmapj2N  30663  osumcllem5N  30694  osumcllem7N  30696  osumcllem10N  30699  lhp0lt  30737  lhpexle1  30742  lhpexle2lem  30743  lhpexle3lem  30745  lhpj1  30756  lhpmcvr5N  30761  lhpat4N  30778  4atexlem7  30809  4atex3  30815  ldilcnv  30849  ldilco  30850  ltrnatb  30871  ltrnel  30873  ltrncnvel  30876  ltrn11at  30881  ltrnmw  30885  trlval2  30897  trljat2  30901  trlat  30903  trl0  30904  trlnidat  30907  trlnidatb  30911  trlval3  30921  cdlemc1  30925  cdlemc2  30926  cdlemd8  30939  cdlemd9  30940  cdleme0ex2N  30958  cdleme7b  30978  cdleme7d  30980  cdleme10  30988  cdleme11dN  30996  cdleme11e  30997  cdleme21h  31068  cdleme26ee  31094  cdlemefr29bpre0N  31140  cdlemefr29clN  31141  cdlemefr32fvaN  31143  cdlemefr32fva1  31144  cdlemefs29bpre0N  31150  cdlemefs29bpre1N  31151  cdlemefs29cpre1N  31152  cdlemefs29clN  31153  cdlemefs32fvaN  31156  cdlemefs32fva1  31157  cdleme32fva  31171  cdleme32fvaw  31173  cdleme32le  31181  cdleme38m  31197  cdleme39a  31199  cdleme17d3  31230  cdlemeg49le  31245  cdlemeg46fvaw  31250  cdlemf1  31295  cdlemfnid  31298  cdlemg2ce  31326  cdlemb3  31340  cdlemg7fvbwN  31341  cdlemg4b1  31343  cdlemg7aN  31359  cdlemg10bALTN  31370  cdlemg12b  31378  cdlemg12d  31380  cdlemg12f  31382  cdlemg12g  31383  cdlemg13  31386  cdlemg31c  31433  cdlemg34  31446  cdlemg36  31448  trlcone  31462  cdlemg44  31467  cdlemg48  31471  tendococl  31506  tendoicl  31530  tendocan  31558  cdlemk7  31582  cdlemk12  31584  cdlemk12u  31606  cdlemk26b-3  31639  cdlemk26-3  31640  cdlemk11ta  31663  cdlemk19ylem  31664  cdlemkid3N  31667  cdlemk11tc  31679  cdlemk11t  31680  cdlemk45  31681  cdlemk46  31682  cdlemk49  31685  cdlemk54  31692  cdlemk55b  31694  cdlemk56  31705  cdlemk19w  31706  cdleml3N  31712  cdleml4N  31713  cdleml6  31715  cdleml7  31716  cdleml8  31717  erngdvlem4-rN  31733  tendocnv  31756  tendospcanN  31758  dia2dimlem12  31810  tendoinvcl  31839  tendolinv  31840  tendorinv  31841  dvhopellsm  31852  dicvaddcl  31925  dicvscacl  31926  cdlemn3  31932  cdlemn4  31933  cdlemn4a  31934  dihord2cN  31956  dihord11c  31959  dih1dimb2  31976  dihvalcq2  31982  dihord5b  31994  dihord5apre  31997  dihglblem2N  32029  dihjatc1  32046  dihmeetlem20N  32061  dihmeetALTN  32062  dih1dimatlem0  32063  dihatexv  32073  dochss  32100  dochdmj1  32125  dvh4dimlem  32178  dvh3dim3N  32184  dochsatshpb  32187  dochexmidlem4  32198  dochexmidlem5  32199  dochexmidlem8  32202  dochkr1  32213  dochkr1OLDN  32214  lcfl7lem  32234  lcfl8  32237  lcfrlem16  32293  lcfrlem40  32317  mapdval2N  32365  mapdpglem24  32439  mapdh6iN  32479  mapdh8ad  32514  mapdh8e  32519  hdmap1fval  32532  hdmap1l6i  32554  hdmapfval  32565  hdmapval0  32571  hdmapevec  32573  hdmapval3N  32576  hdmap10lem  32577  hdmap11lem2  32580  hdmaprnlem15N  32599  hdmaprnlem16N  32600  hdmap14lem10  32615  hdmap14lem11  32616  hdmap14lem12  32617  hgmapfval  32624  hgmapval1  32631  hgmapadd  32632  hgmapmul  32633  hgmaprnlem3N  32636  hgmaprnlem4N  32637  hgmap11  32640  hlhilsrnglem  32691  hlhilphllem  32697
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator