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

Theorem simp2 959
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 955 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simprd 451 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  simpl2  962  simpr2  965  simp2i  968  simp2d  971  simp12  989  simp22  992  simp32  995  syld3an3  1230  intn3an2d  1295  disjss3  4214  nlim0  4642  reusv6OLD  4737  tfisi  4841  feq123  5587  fresaun  5617  fvmptt  5823  fsnunf2  5935  fnsuppres  5955  fnfvima  5979  cocan1  6027  cocan2  6028  fveqf1o  6032  knatar  6083  ovmpt2x  6205  ovmpt2ga  6206  sorpssuni  6534  sorpssint  6535  onoviun  6608  smo11  6629  omeulem1  6828  oeord  6834  oecan  6835  domss2  7269  mapxpen  7276  mapdom3  7282  fofinf1o  7390  elfir  7423  ordtype2  7506  wemapso2  7524  wdomima2g  7557  ixpiunwdom  7562  oemapvali  7643  cnfcom3clem  7665  tcrank  7813  fodomfi2  7946  cdaassen  8067  xpcdaen  8068  mapcdaen  8069  infcdaabs  8091  infdif  8094  ackbij1lem16  8120  cfeq0  8141  cfsuc  8142  isfin2-2  8204  fin23lem26  8210  domtriomlem  8327  axdc3lem2  8336  axdc3lem4  8338  axdc4lem  8340  zornn0g  8390  ttukey2g  8401  canthwe  8531  gchaleph  8551  gchaleph2  8552  gchhar  8559  wunpw  8587  tsktrss  8641  tskcard  8661  tskwun  8664  tskxp  8667  tskmap  8668  tskurn  8669  gruixp  8689  enqeq  8816  ltadd2  9182  readdcan  9245  subadd2  9314  nppcan  9329  nppcan3  9330  subsub2  9334  subsub4  9339  npncan3  9344  pnpcan  9345  pnncan  9347  subcan  9361  ltadd1  9500  leadd1  9501  leadd2  9502  ltsubadd  9503  ltsubadd2  9504  lesubadd  9505  lesubadd2  9506  lesub1  9527  lesub2  9528  ltsub1  9529  ltsub2  9530  mulcan  9664  mulcan2  9665  divmul  9686  divcan1  9692  diveq0  9693  divrec  9699  divass  9701  div23  9702  divdir  9706  divcan3  9707  div11  9709  diveq1  9713  divmuldiv  9719  divcan5  9721  redivcl  9738  div2neg  9742  ltmul1  9865  ltdiv1  9879  ledivmulOLD  9889  ledivmul2OLD  9893  lemuldiv  9894  lt2msq1  9898  ltdiv23  9906  lediv23  9907  infmrlb  9994  ofsubeq0  10002  ofnegsub  10003  ofsubge0  10004  zsupss  10570  suprzub  10572  rpgecl  10642  xrmaxlt  10774  xrltmin  10775  xrmaxle  10776  xrlemin  10777  xleadd1  10839  xltadd1  10840  xlemul1  10874  xlemul2  10875  xltmul1  10876  xadddir  10880  supxrre  10911  infmxrre  10919  ixxub  10942  icc0  10969  ubioc1  10970  ubicc2  11019  icoshftf1o  11025  snunioo  11028  snunico  11029  iccsplit  11034  fzm1  11132  flwordi  11224  flword2  11225  modcyc  11281  axdc4uzlem  11326  expgt1  11423  exprec  11426  expmulz  11431  leexp2a  11440  expubnd  11445  bernneq2  11511  expmulnbnd  11516  digit2  11517  swrdval  11769  ccatco  11809  s3cl  11846  swrds2  11885  shftuz  11889  cjdiv  11974  resqrcl  12064  absdiv  12105  caubnd  12167  limsuple  12277  limsuplt  12278  climuni  12351  iseraltlem3  12482  geoisum1c  12662  eflt  12723  dvdsval2  12860  dvdsadd2b  12897  dvdsexp  12910  dvdsgcdb  13049  mulgcd  13051  gcddiv  13054  mulgcddvds  13109  qredeq  13111  rpexp12i  13127  fermltl  13178  prmdiv  13179  odzcllem  13183  odzphi  13187  coprimeprodsq  13188  pythagtriplem6  13200  pythagtriplem7  13201  pythagtriplem13  13206  pceu  13225  pcgcd1  13255  vdwpc  13353  hashbcss  13377  ramval  13381  0ram2  13394  0ramcl  13396  isstruct2  13483  ressbas  13524  imasvscaval  13768  xpsadd  13806  xpsmul  13807  mrerintcl  13827  ismred2  13833  mremre  13834  mrieqv2d  13869  mreexmrid  13873  cofuass  14091  cofulid  14092  cofurid  14093  catcisolem  14266  posasymb  14414  ple1  14478  latleeqj1  14497  latleeqm1  14513  latnlemlt  14518  ipodrsfi  14594  mrelatglb  14615  mrelatlub  14617  imasmnd2  14737  imasmnd  14738  pwspjmhm  14772  frmdss2  14813  frmdup3  14816  grpinvadd  14872  grpsubeq0  14880  grppncan  14884  grpsubpropd2  14895  mulgnn0p1  14906  mulgnnsubcl  14907  mulgnn0subcl  14908  mulgsubcl  14909  mulgneg  14913  submmulg  14930  pwsinvg  14935  imasgrp2  14938  imasgrp  14939  subgcl  14959  subgsubcl  14960  subgsub  14961  subgmulg  14963  nsgconj  14978  cycsubg2cl  14983  nsgid  14991  ghmmulg  15023  ghmeqker  15037  odcong  15192  oddvds2  15207  odsubdvds  15210  pgpssslw  15253  slwn0  15254  sylow2blem1  15259  lsmssv  15282  lsmsubm  15292  lsmsubg  15293  subglsm  15310  lsmpropd  15314  pj1fval  15331  efgsval2  15370  frgp0  15397  frgpup3  15415  ablinvadd  15439  ablsub4  15442  ablpncan2  15445  subgabl  15460  cntzcmn  15464  gex2abl  15471  lsmsubg2  15479  prdscmnd  15481  ablfacrp  15629  rngidss  15695  rngcom  15697  gsumdixp  15720  imasrng  15730  unitmulcl  15774  unitmulclb  15775  dvrcan1  15801  dvrcan3  15802  irredrmul  15817  subrgmcl  15885  subrgdv  15890  cntzsubr  15905  isabvd  15913  islmod  15959  lmodcom  15995  lssvnegcl  16037  lssintcl  16045  lspss  16065  lspun  16068  lspsnvsi  16085  lmodvsinv  16117  lmodvsinv2  16118  0lmhm  16121  lmhmvsca  16126  reslmhm2  16134  lbsind2  16158  lsmsp  16163  lspsntri  16174  lsmcv  16218  lvecdim  16234  lbsextlem2  16236  lbsextg  16239  rrgeq0  16355  domneq0  16362  domnrrg  16365  aspss  16396  asclmul1  16403  asclmul2  16404  psrbagaddcl  16440  psrbagconcl  16443  psrgrp  16467  psrlmod  16470  psrrng  16479  psrcrng  16481  evlslem4  16569  psrplusgpropd  16634  psropprmul  16637  coe1add  16662  coe1mul2  16667  ply1tmcl  16669  coe1tm  16670  coe1tmfv1  16671  coe1sclmul  16679  coe1sclmul2  16681  chrcong  16815  zndvds  16835  ipeq0  16874  ip2eq  16889  cssmre  16925  obselocv  16960  clsndisj  17144  iscldtop  17164  lpss3  17213  islp3  17215  restabs  17234  restcldi  17242  neitr  17249  restlp  17252  mnfnei  17290  lmconst  17330  cnrest2  17355  cnpresti  17357  hausnei2  17422  sshauslem  17441  cmpcld  17470  fiuncmp  17472  hauscmp  17475  concompclo  17503  2ndc1stc  17519  nllyrest  17554  kgen2ss  17592  xkopjcn  17693  xkococn  17697  cnmpt2t  17710  elqtop  17734  r0cld  17775  cmphaushmeo  17837  filss  17890  isfild  17895  fbasweak  17902  snfbas  17903  trfg  17928  trnei  17929  supfil  17932  ufinffr  17966  ufilen  17967  flimrest  18020  flimclslem  18021  lmflf  18042  fclsneii  18054  fclsrest  18061  cnpfcfi  18077  ptcmpg  18093  istgp2  18126  tgpconcompeqg  18146  prdstmdd  18158  tsmsxp  18189  ustssel  18240  ustn0  18255  ressusp  18300  cfiluweak  18330  neipcfilu  18331  psmetsym  18346  psmetge0  18348  xmetge0  18379  xmetsym  18382  blvalps  18420  blval  18421  xblcntrps  18445  xblcntr  18446  xmssym  18500  blsscls2  18539  stdbdxmet  18550  prdsxms  18565  prdsms  18566  metustblOLD  18615  metustbl  18616  restmetu  18622  isngp4  18663  nmmtri  18673  nmsub  18674  nmrtri  18675  nmtri  18677  nlmmul0or  18724  nmods  18783  xrsmopn  18848  iccntr  18857  metds0  18885  cncfmptc  18946  iirev  18959  icoopnst  18969  iocopnst  18970  icchmeo  18971  iccpnfhmeo  18975  pi1grplem  19079  pi1xfr  19085  isclmi  19107  cphreccllem  19146  ipcau  19200  nmpar  19202  fmcfil  19230  iscau2  19235  cfilres  19254  caussi  19255  caublcls  19266  bcthlem5  19286  srabn  19319  rlmbn  19320  pjth  19345  pjth2  19346  cniccbdd  19363  ovolgelb  19381  ovollecl  19384  ovolunnul  19401  ovolicc  19424  cmmbl  19434  iundisj2  19448  voliunlem2  19450  voliunlem3  19451  ovolioo  19467  volcn  19503  cncombf  19553  itg1le  19608  itg2lecl  19633  itgconst  19713  bddibl  19734  dvfval  19789  dvid  19809  dvcnp  19810  dvcnp2  19811  dvnf  19818  dvnbss  19819  dvn2bss  19821  evlsval2  19946  mdegldg  19994  deg1lt  20025  deg1mul3  20043  deg1mul3le  20044  q1peqb  20082  r1pcl  20085  r1pdeglt  20086  r1pid  20087  dvdsr1p  20089  fta1b  20097  drnguc1p  20098  ig1peu  20099  elplyr  20125  dgrub  20158  dgrlb  20160  dgradd2  20191  ofmulrt  20204  quotcl2  20224  quotdgr  20225  quotcan  20231  vieta1  20234  aannenlem1  20250  aannenlem2  20251  aalioulem3  20256  aaliou2  20262  ulmcl  20302  tanord1  20444  tanord  20445  cxpef  20561  cxpadd  20575  cxpneg  20577  cxpsub  20578  divcxp  20583  cxpmul  20584  cxpeq  20646  ang180lem1  20656  ang180lem2  20657  ang180lem3  20658  ang180lem4  20659  angpieqvd  20677  xrlimcnp  20812  cxp2lim  20820  wilthlem3  20858  chtwordi  20944  ppiwordi  20950  sgmppw  20986  dchrabl  21043  bcmono  21066  efexple  21070  lgsneg1  21109  lgsmod  21110  lgssq  21124  lgsdirnn0  21128  lgsdinn0  21129  lgsqrlem5  21134  lgsquad  21146  dirith  21228  pntrmax  21263  abvcxp  21314  cusgra3v  21478  2trllemE  21558  1pthon  21596  2pthon  21607  grpoasscan2  21831  grpoinvop  21834  grpopncan  21844  grponpcan  21845  gxcom  21862  gxinv  21863  gxsuc  21865  gxdi  21889  rngodi  21978  rngosn  21997  zerdivemp1  22027  nvpncan2  22142  nvnncan  22149  nvs  22156  nvdif  22159  nvpi  22160  nvabs  22167  nv1  22170  lno0  22262  lnocoi  22263  nmooge0  22273  shlub  22921  pjspansn  23084  adj2  23442  kbmul  23463  adjlnop  23594  cdj3lem3a  23947  iundisj2f  24035  curry2ima  24102  snunioc  24142  iocinioc2  24147  iundisj2fi  24158  divnumden2  24166  xreceu  24173  xdivcl  24175  xdivmul  24176  xdivrec  24178  ress0g  24187  tleile  24194  xrsmulgzz  24205  xrge0addass  24216  xrge0neqmnf  24217  cnre2csqlem  24313  nmmulg  24357  qqhval2lem  24370  relogbcl  24407  logb1  24408  logblt  24411  ind1  24421  esummulc1  24476  hasheuni  24480  sigaclcu  24505  difelsiga  24521  elsigagen2  24536  sigagenss2  24538  isrnmeas  24559  measvun  24568  measvunilem  24571  measvunilem0  24572  measvuni  24573  measres  24581  aean  24600  mbfmco2  24620  dya2icoseg2  24633  sitgclg  24661  totprob  24690  probmeasb  24693  cndprobval  24696  cndprobnul  24700  cndprobprob  24701  bayesth  24702  orvclteinc  24738  lgamgulmlem1  24818  cvmcov2  24967  dedekind  25192  dedekindle  25193  subdivcomb2  25201  binomrisefac  25363  predeq123  25445  trpredpo  25518  wsuceq123  25570  wzel  25580  elno2  25614  brbtwn2  25849  colinearalglem1  25850  colinearalglem2  25851  axcgrid  25860  ax5seglem2  25873  axbtwnid  25883  axpasch  25885  axcontlem4  25911  axcontlem8  25915  cgrrflx  25926  cgrtriv  25941  btwntriv2  25951  btwntriv1  25955  trisegint  25967  btwnxfr  25995  colineardim1  26000  colineartriv1  26006  colineartriv2  26007  btwnconn1lem7  26032  segcon2  26044  seglerflx  26051  outsidene2  26063  liness  26084  hilbert1.1  26093  bpolycl  26103  areacirclem2  26307  areacirclem5  26310  areacirc  26311  comppfsc  26401  mettrifi  26477  cnresima  26487  ismtybndlem  26529  rrnmval  26551  zerdivemp1x  26585  isfldidl  26692  ismrcd1  26766  istopclsd  26768  ismrc  26769  mapfzcons  26786  mzpcl34  26802  mzpexpmpt  26816  mzpsubst  26819  eldioph  26830  diophrw  26831  pellexlem5  26910  pellex  26912  pell14qrgap  26952  pellfundlb  26961  pellfundglb  26962  pellfundex  26963  rmxycomplete  26994  rmxyadd  26998  monotoddzz  27020  rmxypos  27026  rmygeid  27043  acongrep  27059  acongeq  27062  coprmdvdsb  27066  modabsdifz  27070  dvdsabsmod0  27071  jm2.22  27080  rmydioph  27099  rmxdioph  27101  expdiophlem2  27107  rpnnen3lem  27116  pwssplit0  27178  pwssplit1  27179  pwssplit2  27180  pwssplit3  27181  pwssplit4  27182  dsmmsubg  27200  uvcresum  27233  frlmsplit2  27234  frlmsslss  27235  frlmup4  27244  isnumbasgrplem2  27260  islindf2  27275  lindfind2  27279  hbtlem2  27319  mpaaeu  27346  pmtrmvd  27389  pmtrfrn  27391  pmtrfb  27397  psgnunilem4  27411  matrng  27471  idomrootle  27502  fiuneneq  27504  proot1hash  27510  ofdivrec  27534  ofdivcan4  27535  ubelsupr  27681  fmul01  27700  fmuldfeq  27703  fmul01lt1lem2  27705  fmul01lt1  27706  climsuse  27724  stoweidlem3  27742  stoweidlem6  27745  stoweidlem8  27747  stoweidlem10  27749  stoweidlem19  27758  stoweidlem26  27765  stoweidlem28  27767  stoweidlem31  27770  stoweidlem57  27796  stoweidlem59  27798  stoweidlem60  27799  wallispilem3  27806  stirlinglem13  27825  sigaraf  27833  sigarmf  27834  sigaras  27835  sigarms  27836  sigarls  27837  sigarexp  27839  sigarperm  27840  sigarcol  27844  ssfzo12  28153  el2fzo  28161  ltdifltdiv  28171  modsubmod  28178  modsubmodmod  28179  ccatsymb  28211  swrd0fv  28226  swrd0swrd  28231  cshwidxm1  28279  2cshw2lem2  28287  3cshw  28303  usgra2wlkspth  28346  el2wlkonotot0  28404  vdn0frgrav2  28488  vdn1frgrav2  28490  3orbi123  28668  alrim3con13v  28691  3orbi123VD  29036  19.21a3con13vVD  29038  tratrbVD  29047  bnj906  29375  bnj1110  29425  bnj1128  29433  bnj1145  29436  bnj1189  29452  bnj1204  29455  bnj1279  29461  bnj1311  29467  bnj1408  29479  toycom  29844  lshpnelb  29856  lsatfixedN  29881  lssatomic  29883  lcvat  29902  lsatcveq0  29904  lcvexchlem4  29909  lcvexchlem5  29910  lsatcvatlem  29921  islshpcv  29925  l1cvpat  29926  lfladd  29938  lflsub  29939  lflmul  29940  lfl1  29942  eqlkr  29971  lkrshp  29977  lshpsmreu  29981  lshpkrex  29990  ldualgrplem  30017  lduallmodlem  30024  lkrlspeqN  30043  oldmm1  30089  olj01  30097  omllaw4  30118  omllaw5N  30119  cmt2N  30122  cmt3N  30123  cmtbr2N  30125  cmtbr3N  30126  cmtbr4N  30127  lecmtN  30128  meetat  30168  atn0  30180  cvlcvr1  30211  cvlcvrp  30212  cvlsupr6  30219  hlrelat2  30274  exatleN  30275  cvr2N  30282  hlrelat3  30283  cvrval3  30284  cvrval4N  30285  cvrval5  30286  cvrexch  30291  lnnat  30298  atle  30307  atlt  30308  2atlt  30310  atbtwnexOLDN  30318  atbtwnex  30319  1cvratlt  30345  ps-2b  30353  3atlem5  30358  llnnleat  30384  llnle  30389  llnexatN  30392  llncmp  30393  2llnmat  30395  lplni2  30408  lvolex3N  30409  lplnle  30411  lplnnleat  30413  lplncmp  30433  lplnexatN  30434  2atnelvolN  30458  4atlem10  30477  4atlem11  30480  4atlem12  30483  lvolcmp  30488  dalemswapyz  30527  dalemswapyzps  30561  dalem56  30599  pmaple  30632  lneq2at  30649  lnjatN  30651  lncmp  30654  2lnat  30655  elpadd2at  30677  pmapjat1  30724  pmapjat2  30725  dalawlem10  30751  dalawlem13  30754  dalawlem15  30756  dalaw  30757  elpcliN  30764  pclunN  30769  polcon3N  30788  paddunN  30798  poldmj1N  30799  pmapj2N  30800  osumcllem5N  30831  osumcllem7N  30833  osumcllem10N  30836  lhp0lt  30874  lhpexle1  30879  lhpexle2lem  30880  lhpexle3lem  30882  lhpj1  30893  lhpmcvr5N  30898  lhpat4N  30915  4atexlem7  30946  4atex3  30952  ldilcnv  30986  ldilco  30987  ltrnatb  31008  ltrnel  31010  ltrncnvel  31013  ltrn11at  31018  ltrnmw  31022  trlval2  31034  trljat2  31038  trlat  31040  trl0  31041  trlnidat  31044  trlnidatb  31048  trlval3  31058  cdlemc1  31062  cdlemc2  31063  cdlemd8  31076  cdlemd9  31077  cdleme0ex2N  31095  cdleme7b  31115  cdleme7d  31117  cdleme10  31125  cdleme11dN  31133  cdleme11e  31134  cdleme21h  31205  cdleme26ee  31231  cdlemefr29bpre0N  31277  cdlemefr29clN  31278  cdlemefr32fvaN  31280  cdlemefr32fva1  31281  cdlemefs29bpre0N  31287  cdlemefs29bpre1N  31288  cdlemefs29cpre1N  31289  cdlemefs29clN  31290  cdlemefs32fvaN  31293  cdlemefs32fva1  31294  cdleme32fva  31308  cdleme32fvaw  31310  cdleme32le  31318  cdleme38m  31334  cdleme39a  31336  cdleme17d3  31367  cdlemeg49le  31382  cdlemeg46fvaw  31387  cdlemf1  31432  cdlemfnid  31435  cdlemg2ce  31463  cdlemb3  31477  cdlemg7fvbwN  31478  cdlemg4b1  31480  cdlemg7aN  31496  cdlemg10bALTN  31507  cdlemg12b  31515  cdlemg12d  31517  cdlemg12f  31519  cdlemg12g  31520  cdlemg13  31523  cdlemg31c  31570  cdlemg34  31583  cdlemg36  31585  trlcone  31599  cdlemg44  31604  cdlemg48  31608  tendococl  31643  tendoicl  31667  tendocan  31695  cdlemk7  31719  cdlemk12  31721  cdlemk12u  31743  cdlemk26b-3  31776  cdlemk26-3  31777  cdlemk11ta  31800  cdlemk19ylem  31801  cdlemkid3N  31804  cdlemk11tc  31816  cdlemk11t  31817  cdlemk45  31818  cdlemk46  31819  cdlemk49  31822  cdlemk54  31829  cdlemk55b  31831  cdlemk56  31842  cdlemk19w  31843  cdleml3N  31849  cdleml4N  31850  cdleml6  31852  cdleml7  31853  cdleml8  31854  erngdvlem4-rN  31870  tendocnv  31893  tendospcanN  31895  dia2dimlem12  31947  tendoinvcl  31976  tendolinv  31977  tendorinv  31978  dvhopellsm  31989  dicvaddcl  32062  dicvscacl  32063  cdlemn3  32069  cdlemn4  32070  cdlemn4a  32071  dihord2cN  32093  dihord11c  32096  dih1dimb2  32113  dihvalcq2  32119  dihord5b  32131  dihord5apre  32134  dihglblem2N  32166  dihjatc1  32183  dihmeetlem20N  32198  dihmeetALTN  32199  dih1dimatlem0  32200  dihatexv  32210  dochss  32237  dochdmj1  32262  dvh4dimlem  32315  dvh3dim3N  32321  dochsatshpb  32324  dochexmidlem4  32335  dochexmidlem5  32336  dochexmidlem8  32339  dochkr1  32350  dochkr1OLDN  32351  lcfl7lem  32371  lcfl8  32374  lcfrlem16  32430  lcfrlem40  32454  mapdval2N  32502  mapdpglem24  32576  mapdh6iN  32616  mapdh8ad  32651  mapdh8e  32656  hdmap1fval  32669  hdmap1l6i  32691  hdmapfval  32702  hdmapval0  32708  hdmapevec  32710  hdmapval3N  32713  hdmap10lem  32714  hdmap11lem2  32717  hdmaprnlem15N  32736  hdmaprnlem16N  32737  hdmap14lem10  32752  hdmap14lem11  32753  hdmap14lem12  32754  hgmapfval  32761  hgmapval1  32768  hgmapadd  32769  hgmapmul  32770  hgmaprnlem3N  32773  hgmaprnlem4N  32774  hgmap11  32777  hlhilsrnglem  32828  hlhilphllem  32834
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator