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  4022  nlim0  4450  reusv6OLD  4545  tfisi  4649  fresaun  5412  fvmptt  5615  fsnunf2  5719  fnsuppres  5732  fnfvima  5756  cocan1  5801  cocan2  5802  fveqf1o  5806  knatar  5857  ovmpt2x  5976  ovmpt2ga  5977  sorpssuni  6286  sorpssint  6287  onoviun  6360  smo11  6381  omeulem1  6580  oeord  6586  oecan  6587  domss2  7020  mapxpen  7027  mapdom3  7033  fofinf1o  7137  elfir  7169  ordtype2  7249  wemapso2  7267  wdomima2g  7300  ixpiunwdom  7305  oemapvali  7386  cnfcom3clem  7408  tcrank  7554  fodomfi2  7687  cdaassen  7808  xpcdaen  7809  mapcdaen  7810  infcdaabs  7832  infdif  7835  ackbij1lem16  7861  cfeq0  7882  cfsuc  7883  isfin2-2  7945  fin23lem26  7951  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  zornn0g  8132  ttukey2g  8143  canthwe  8273  gchhar  8293  gchaleph  8297  gchaleph2  8298  wunpw  8329  tsktrss  8383  tskcard  8403  tskwun  8406  tskxp  8409  tskmap  8410  tskurn  8411  gruixp  8431  enqeq  8558  ltadd2  8924  readdcan  8986  subadd2  9055  nppcan  9070  nppcan3  9071  subsub2  9075  subsub4  9080  npncan3  9085  pnpcan  9086  pnncan  9088  subcan  9102  ltadd1  9241  leadd1  9242  leadd2  9243  ltsubadd  9244  ltsubadd2  9245  lesubadd  9246  lesubadd2  9247  lesub1  9268  lesub2  9269  ltsub1  9270  ltsub2  9271  mulcan  9405  mulcan2  9406  divmul  9427  divcan1  9433  diveq0  9434  divrec  9440  divass  9442  div23  9443  divdir  9447  divcan3  9448  div11  9450  diveq1  9454  divmuldiv  9460  divcan5  9462  redivcl  9479  div2neg  9483  ltmul1  9606  ltdiv1  9620  ledivmulOLD  9630  ledivmul2OLD  9634  lemuldiv  9635  lt2msq1  9639  ltdiv23  9647  lediv23  9648  infmrlb  9735  ofsubeq0  9743  ofnegsub  9744  ofsubge0  9745  zsupss  10307  suprzub  10309  rpgecl  10379  xrmaxlt  10510  xrltmin  10511  xrmaxle  10512  xrlemin  10513  xleadd1  10575  xltadd1  10576  xlemul1  10610  xlemul2  10611  xltmul1  10612  xadddir  10616  supxrre  10646  infmxrre  10654  ixxub  10677  icc0  10704  ubioc1  10705  ubicc2  10753  icoshftf1o  10759  snunioo  10762  snunico  10763  iccsplit  10768  fzm1  10862  flwordi  10942  flword2  10943  modcyc  10999  axdc4uzlem  11044  expgt1  11140  exprec  11143  expmulz  11148  leexp2a  11157  expubnd  11162  bernneq2  11228  expmulnbnd  11233  digit2  11234  swrdval  11450  ccatco  11490  s3cl  11527  swrds2  11560  shftuz  11564  cjdiv  11649  resqrcl  11739  absdiv  11780  caubnd  11842  limsuple  11952  limsuplt  11953  climuni  12026  iseraltlem3  12156  geoisum1c  12336  eflt  12397  dvdsval2  12534  dvdsadd2b  12571  dvdsexp  12584  dvdsgcdb  12723  mulgcd  12725  gcddiv  12728  mulgcddvds  12783  qredeq  12785  rpexp12i  12801  fermltl  12852  prmdiv  12853  odzcllem  12857  odzphi  12861  coprimeprodsq  12862  pythagtriplem6  12874  pythagtriplem7  12875  pythagtriplem13  12880  pceu  12899  pcgcd1  12929  vdwpc  13027  hashbcss  13051  ramval  13055  0ram2  13068  0ramcl  13070  isstruct2  13157  ressbas  13198  imasvscaval  13440  xpsadd  13478  xpsmul  13479  mrerintcl  13499  ismred2  13505  mremre  13506  mrieqv2d  13541  mreexmrid  13545  cofuass  13763  cofulid  13764  cofurid  13765  catcisolem  13938  posasymb  14086  ple1  14150  latleeqj1  14169  latleeqm1  14185  latnlemlt  14190  ipodrsfi  14266  mrelatglb  14287  mrelatlub  14289  imasmnd2  14409  imasmnd  14410  pwspjmhm  14444  frmdss2  14485  frmdup3  14488  grpinvadd  14544  grpsubeq0  14552  grppncan  14556  grpsubpropd2  14567  mulgnn0p1  14578  mulgnnsubcl  14579  mulgnn0subcl  14580  mulgsubcl  14581  mulgneg  14585  submmulg  14602  pwsinvg  14607  imasgrp2  14610  imasgrp  14611  subgcl  14631  subgsubcl  14632  subgsub  14633  subgmulg  14635  nsgconj  14650  cycsubg2cl  14655  nsgid  14663  ghmmulg  14695  ghmeqker  14709  odcong  14864  oddvds2  14879  odsubdvds  14882  pgpssslw  14925  slwn0  14926  sylow2blem1  14931  lsmssv  14954  lsmsubm  14964  lsmsubg  14965  subglsm  14982  lsmpropd  14986  pj1fval  15003  efgsval2  15042  frgp0  15069  frgpup3  15087  ablinvadd  15111  ablsub4  15114  ablpncan2  15117  subgabl  15132  cntzcmn  15136  gex2abl  15143  lsmsubg2  15151  prdscmnd  15153  ablfacrp  15301  rngidss  15367  rngcom  15369  gsumdixp  15392  imasrng  15402  unitmulcl  15446  unitmulclb  15447  dvrcan1  15473  dvrcan3  15474  irredrmul  15489  subrgmcl  15557  subrgdv  15562  cntzsubr  15577  isabvd  15585  islmod  15631  lmodvsnegOLD  15668  lmodcom  15671  lssvnegcl  15713  lssintcl  15721  lspss  15741  lspun  15744  lspsnvsi  15761  lmodvsinv  15793  lmodvsinv2  15794  0lmhm  15797  lmhmvsca  15802  reslmhm2  15810  lbsind2  15834  lsmsp  15839  lspsntri  15850  lsmcv  15894  lvecdim  15910  lbsextlem2  15912  lbsextg  15915  rrgeq0  16031  domneq0  16038  domnrrg  16041  aspss  16072  asclmul1  16079  asclmul2  16080  psrbagaddcl  16116  psrbagconcl  16119  psrgrp  16143  psrlmod  16146  psrrng  16155  psrcrng  16157  evlslem4  16245  psrplusgpropd  16313  psropprmul  16316  coe1add  16341  coe1mul2  16346  ply1tmcl  16348  coe1tm  16349  coe1tmfv1  16350  coe1sclmul  16358  coe1sclmul2  16360  chrcong  16483  zndvds  16503  ipeq0  16542  ip2eq  16557  cssmre  16593  obselocv  16628  clsndisj  16812  iscldtop  16832  lpss3  16876  restabs  16896  restcldi  16904  restlp  16913  mnfnei  16951  lmconst  16991  cnrest2  17014  cnpresti  17016  hausnei2  17081  sshauslem  17100  cmpcld  17129  fiuncmp  17131  hauscmp  17134  concompclo  17161  2ndc1stc  17177  nllyrest  17212  kgen2ss  17250  xkopjcn  17350  xkococn  17354  cnmpt2t  17367  elqtop  17388  r0cld  17429  cmphaushmeo  17491  filss  17548  isfild  17553  fbasweak  17560  snfbas  17561  trfg  17586  trnei  17587  supfil  17590  ufinffr  17624  ufilen  17625  flimrest  17678  flimclslem  17679  lmflf  17700  fclsneii  17712  fclsrest  17719  cnpfcfi  17735  ptcmpg  17751  istgp2  17774  tgpconcompeqg  17794  prdstmdd  17806  tsmsxp  17837  xmetge0  17909  xmetsym  17912  blval  17948  xblcntr  17963  xmssym  18011  blsscls2  18050  stdbdxmet  18061  prdsxms  18076  prdsms  18077  isngp4  18133  nmmtri  18143  nmsub  18144  nmrtri  18145  nmtri  18147  nlmmul0or  18194  nmods  18253  xrsmopn  18318  iccntr  18326  metds0  18354  cncfmptc  18415  iirev  18427  icoopnst  18437  iocopnst  18438  icchmeo  18439  iccpnfhmeo  18443  pi1grplem  18547  pi1xfr  18553  isclmi  18575  cphreccllem  18614  ipcau  18668  nmpar  18670  fmcfil  18698  iscau2  18703  cfilres  18722  caussi  18723  caublcls  18734  bcthlem5  18750  srabn  18777  rlmbn  18778  pjth  18803  pjth2  18804  cniccbdd  18821  ovolgelb  18839  ovollecl  18842  ovolunnul  18859  ovolicc  18882  cmmbl  18892  iundisj2  18906  voliunlem2  18908  voliunlem3  18909  ovolioo  18925  volcn  18961  cncombf  19013  itg1le  19068  itg2lecl  19093  itgconst  19173  bddibl  19194  dvfval  19247  dvid  19267  dvcnp  19268  dvcnp2  19269  dvnf  19276  dvnbss  19277  dvn2bss  19279  evlsval2  19404  mdegldg  19452  deg1lt  19483  deg1mul3  19501  deg1mul3le  19502  q1peqb  19540  r1pcl  19543  r1pdeglt  19544  r1pid  19545  dvdsr1p  19547  fta1b  19555  drnguc1p  19556  ig1peu  19557  elplyr  19583  dgrub  19616  dgrlb  19618  dgradd2  19649  ofmulrt  19662  quotcl2  19682  quotdgr  19683  quotcan  19689  vieta1  19692  aannenlem1  19708  aannenlem2  19709  aalioulem3  19714  aaliou2  19720  ulmcl  19760  tanord1  19899  tanord  19900  cxpef  20012  cxpadd  20026  cxpneg  20028  cxpsub  20029  divcxp  20034  cxpmul  20035  cxpeq  20097  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  ang180lem4  20110  angpieqvd  20128  xrlimcnp  20263  cxp2lim  20271  wilthlem3  20308  chtwordi  20394  ppiwordi  20400  sgmppw  20436  dchrabl  20493  bcmono  20516  efexple  20520  lgsneg1  20559  lgsmod  20560  lgssq  20574  lgsdirnn0  20578  lgsdinn0  20579  lgsqrlem5  20584  lgsquad  20596  dirith  20678  pntrmax  20713  abvcxp  20764  grpoasscan2  20905  grpoinvop  20908  grpopncan  20918  grponpcan  20919  gxcom  20936  gxinv  20937  gxsuc  20939  gxdi  20963  rngodi  21052  rngosn  21071  nvpncan2  21214  nvnncan  21221  nvs  21228  nvdif  21231  nvpi  21232  nvabs  21239  nv1  21242  lno0  21334  lnocoi  21335  nmooge0  21345  shlub  21993  pjspansn  22156  adj2  22514  kbmul  22535  adjlnop  22666  cdj3lem3a  23019  xreceu  23105  xdivcl  23107  xdivmul  23108  xdivrec  23110  curry2ima  23247  snunioc  23267  iocinioc2  23272  cnre2csqlem  23294  xrsmulgzz  23307  xrge0addass  23329  xrge0neqmnf  23330  xrge0adddir  23332  iundisj2fi  23364  iundisj2f  23366  relogbcl  23404  logb1  23405  logblt  23408  esummulc1  23449  hasheuni  23453  sigaclcu  23478  difelsiga  23494  elsigagen2  23509  isrnmeas  23531  measvun  23537  measxun2  23538  measvunilem  23540  measvunilem0  23541  measvuni  23542  measres  23549  mbfmco2  23570  ind1  23602  probun  23622  totprob  23630  probmeasb  23633  cndprobval  23636  cndprobtot  23639  cndprobnul  23640  cndprobprob  23641  bayesth  23642  orvclteinc  23676  cvmcov2  23806  dedekind  24082  dedekindle  24083  subdivcomb2  24091  trpredpo  24238  elno2  24308  brbtwn2  24533  colinearalglem1  24534  colinearalglem2  24535  axcgrid  24544  ax5seglem2  24557  axbtwnid  24567  axpasch  24569  axcontlem4  24595  axcontlem8  24599  cgrrflx  24610  cgrtriv  24625  btwntriv2  24635  btwntriv1  24639  trisegint  24651  btwnxfr  24679  colineardim1  24684  colineartriv1  24690  colineartriv2  24691  btwnconn1lem7  24716  segcon2  24728  seglerflx  24735  outsidene2  24747  liness  24768  hilbert1.1  24777  bpolycl  24787  areacirclem4  24927  areacirclem6  24930  areacirc  24931  intn3an2d  24937  infxpg  25095  iccleub2  25135  injsurinj  25149  iscst2  25175  mop  25185  preotr2  25235  altprs2  25236  supdefa  25263  inposet  25278  reacomsmgrp1  25343  reacomsmgrp3  25345  reacomsmgrp4  25346  isppm  25354  mndoass  25359  fprodneg  25378  multinv  25422  multinvb  25423  fldax4  25431  zerdivemp1  25436  mvecrtol2  25477  islp3  25514  mapdiscn  25527  hmeogrpi  25536  istopxc  25548  conttnf2  25562  islimrs3  25581  islimrs4  25582  mslb1  25607  2wsms  25608  msra3  25609  iintlem1  25610  limnumrr  25622  flfneic  25624  lvsovso2  25627  issubrv  25672  ismulcv  25681  distsava  25689  isdivcv2  25693  divclcvd  25694  divclrvd  25695  cmpassoh  25801  imonclem  25813  ismonc  25814  tartarmap  25888  indcls2  25996  elhalop2  26069  isconcl6a  26103  isibg1a2  26117  isibg2a2  26120  isibg1a6  26125  segline  26141  pxysxy  26142  lppotos  26144  rayline  26156  pdiveql  26168  comppfsc  26307  mettrifi  26473  cnresima  26484  ismtybndlem  26530  rrnmval  26552  zerdivemp1x  26586  isfldidl  26693  ismrcd1  26773  istopclsd  26775  ismrc  26776  mapfzcons  26793  mzpcl34  26809  mzpexpmpt  26823  mzpsubst  26826  eldioph  26837  diophrw  26838  pellexlem5  26918  pellex  26920  pell14qrgap  26960  pellfundlb  26969  pellfundglb  26970  pellfundex  26971  rmxycomplete  27002  rmxyadd  27006  monotoddzz  27028  rmxypos  27034  rmygeid  27051  acongrep  27067  acongeq  27070  coprmdvdsb  27074  modabsdifz  27078  dvdsabsmod0  27079  jm2.22  27088  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115  rpnnen3lem  27124  pwssplit0  27187  pwssplit1  27188  pwssplit2  27189  pwssplit3  27190  pwssplit4  27191  dsmmsubg  27209  uvcresum  27242  frlmsplit2  27243  frlmsslss  27244  frlmup4  27253  isnumbasgrplem2  27269  islindf2  27284  lindfind2  27288  hbtlem2  27328  mpaaeu  27355  pmtrmvd  27398  pmtrfrn  27400  pmtrfb  27406  psgnunilem4  27420  matrng  27480  idomrootle  27511  fiuneneq  27513  proot1hash  27519  ofdivrec  27543  ofdivcan4  27544  ubelsupr  27691  fnchoice  27700  refsumcn  27701  fmul01  27710  fmuldfeq  27713  fmul01lt1lem2  27715  fmul01lt1  27716  climsuse  27734  ibliccsinexp  27745  stoweidlem3  27752  stoweidlem6  27755  stoweidlem8  27757  stoweidlem10  27759  stoweidlem17  27766  stoweidlem19  27768  stoweidlem22  27771  stoweidlem26  27775  stoweidlem28  27777  stoweidlem31  27780  stoweidlem34  27783  stoweidlem43  27792  stoweidlem46  27795  stoweidlem48  27797  stoweidlem49  27798  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem55  27804  stoweidlem56  27805  stoweidlem57  27806  stoweidlem58  27807  stoweidlem59  27808  stoweidlem60  27809  stoweid  27812  wallispilem3  27816  stirlinglem13  27835  sigaraf  27843  sigarmf  27844  sigaras  27845  sigarms  27846  sigarls  27847  sigarexp  27849  sigarperm  27850  sigarcol  27854  3orbi123  28273  alrim3con13v  28296  3orbi123VD  28626  19.21a3con13vVD  28628  tratrbVD  28637  bnj906  28962  bnj1110  29012  bnj1128  29020  bnj1145  29023  bnj1189  29039  bnj1204  29042  bnj1279  29048  bnj1311  29054  bnj1408  29066  toycom  29162  lshpnelb  29174  lsatfixedN  29199  lssatomic  29201  lcvat  29220  lsatcveq0  29222  lcvexchlem4  29227  lcvexchlem5  29228  lsatcvatlem  29239  islshpcv  29243  l1cvpat  29244  lfladd  29256  lflsub  29257  lflmul  29258  lfl1  29260  eqlkr  29289  lkrshp  29295  lshpsmreu  29299  lshpkrex  29308  ldualgrplem  29335  lduallmodlem  29342  lkrlspeqN  29361  oldmm1  29407  olj01  29415  omllaw4  29436  omllaw5N  29437  cmt2N  29440  cmt3N  29441  cmtbr2N  29443  cmtbr3N  29444  cmtbr4N  29445  lecmtN  29446  meetat  29486  atn0  29498  cvlcvr1  29529  cvlcvrp  29530  cvlsupr6  29537  hlrelat2  29592  exatleN  29593  cvr2N  29600  hlrelat3  29601  cvrval3  29602  cvrval4N  29603  cvrval5  29604  cvrexch  29609  lnnat  29616  atle  29625  atlt  29626  2atlt  29628  atbtwnexOLDN  29636  atbtwnex  29637  1cvratlt  29663  ps-2b  29671  3atlem5  29676  llnnleat  29702  llnle  29707  llnexatN  29710  llncmp  29711  2llnmat  29713  lplni2  29726  lvolex3N  29727  lplnle  29729  lplnnleat  29731  lplncmp  29751  lplnexatN  29752  2atnelvolN  29776  4atlem10  29795  4atlem11  29798  4atlem12  29801  lvolcmp  29806  dalemswapyz  29845  dalemswapyzps  29879  dalem56  29917  pmaple  29950  lneq2at  29967  lnjatN  29969  lncmp  29972  2lnat  29973  elpadd2at  29995  pmapjat1  30042  pmapjat2  30043  dalawlem10  30069  dalawlem13  30072  dalawlem15  30074  dalaw  30075  elpcliN  30082  pclunN  30087  polcon3N  30106  paddunN  30116  poldmj1N  30117  pmapj2N  30118  osumcllem5N  30149  osumcllem7N  30151  osumcllem10N  30154  lhp0lt  30192  lhpexle1  30197  lhpexle2lem  30198  lhpexle3lem  30200  lhpj1  30211  lhpmcvr5N  30216  lhpat4N  30233  4atexlem7  30264  4atex3  30270  ldilcnv  30304  ldilco  30305  ltrnatb  30326  ltrnel  30328  ltrncnvel  30331  ltrn11at  30336  ltrnmw  30340  trlval2  30352  trljat2  30356  trlat  30358  trl0  30359  trlnidat  30362  trlnidatb  30366  trlval3  30376  cdlemc1  30380  cdlemc2  30381  cdlemd8  30394  cdlemd9  30395  cdleme0ex2N  30413  cdleme7b  30433  cdleme7d  30435  cdleme10  30443  cdleme11dN  30451  cdleme11e  30452  cdleme21h  30523  cdleme26ee  30549  cdlemefr29bpre0N  30595  cdlemefr29clN  30596  cdlemefr32fvaN  30598  cdlemefr32fva1  30599  cdlemefs29bpre0N  30605  cdlemefs29bpre1N  30606  cdlemefs29cpre1N  30607  cdlemefs29clN  30608  cdlemefs32fvaN  30611  cdlemefs32fva1  30612  cdleme32fva  30626  cdleme32fvaw  30628  cdleme32le  30636  cdleme38m  30652  cdleme39a  30654  cdleme17d3  30685  cdlemeg49le  30700  cdlemeg46fvaw  30705  cdlemf1  30750  cdlemfnid  30753  cdlemg2ce  30781  cdlemb3  30795  cdlemg7fvbwN  30796  cdlemg4b1  30798  cdlemg7aN  30814  cdlemg10bALTN  30825  cdlemg12b  30833  cdlemg12d  30835  cdlemg12f  30837  cdlemg12g  30838  cdlemg13  30841  cdlemg31c  30888  cdlemg34  30901  cdlemg36  30903  trlcone  30917  cdlemg44  30922  cdlemg48  30926  tendococl  30961  tendoicl  30985  tendocan  31013  cdlemk7  31037  cdlemk12  31039  cdlemk12u  31061  cdlemk26b-3  31094  cdlemk26-3  31095  cdlemk11ta  31118  cdlemk19ylem  31119  cdlemkid3N  31122  cdlemk11tc  31134  cdlemk11t  31135  cdlemk45  31136  cdlemk46  31137  cdlemk49  31140  cdlemk54  31147  cdlemk55b  31149  cdlemk56  31160  cdlemk19w  31161  cdleml3N  31167  cdleml4N  31168  cdleml6  31170  cdleml7  31171  cdleml8  31172  erngdvlem4-rN  31188  tendocnv  31211  tendospcanN  31213  dia2dimlem12  31265  tendoinvcl  31294  tendolinv  31295  tendorinv  31296  dvhopellsm  31307  dicvaddcl  31380  dicvscacl  31381  cdlemn3  31387  cdlemn4  31388  cdlemn4a  31389  dihord2cN  31411  dihord11c  31414  dih1dimb2  31431  dihvalcq2  31437  dihord5b  31449  dihord5apre  31452  dihglblem2N  31484  dihjatc1  31501  dihmeetlem20N  31516  dihmeetALTN  31517  dih1dimatlem0  31518  dihatexv  31528  dochss  31555  dochdmj1  31580  dvh4dimlem  31633  dvh3dim3N  31639  dochsatshpb  31642  dochexmidlem4  31653  dochexmidlem5  31654  dochexmidlem8  31657  dochkr1  31668  dochkr1OLDN  31669  lcfl7lem  31689  lcfl8  31692  lcfrlem16  31748  lcfrlem40  31772  mapdval2N  31820  mapdpglem24  31894  mapdh6iN  31934  mapdh8ad  31969  mapdh8e  31974  hdmap1fval  31987  hdmap1l6i  32009  hdmapfval  32020  hdmapval0  32026  hdmapevec  32028  hdmapval3N  32031  hdmap10lem  32032  hdmap11lem2  32035  hdmaprnlem15N  32054  hdmaprnlem16N  32055  hdmap14lem10  32070  hdmap14lem11  32071  hdmap14lem12  32072  hgmapfval  32079  hgmapval1  32086  hgmapadd  32087  hgmapmul  32088  hgmaprnlem3N  32091  hgmaprnlem4N  32092  hgmap11  32095  hlhilsrnglem  32146  hlhilphllem  32152
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