MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2 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  disjss3  4171  nlim0  4599  reusv6OLD  4693  tfisi  4797  feq123  5543  fresaun  5573  fvmptt  5779  fsnunf2  5891  fnsuppres  5911  fnfvima  5935  cocan1  5983  cocan2  5984  fveqf1o  5988  knatar  6039  ovmpt2x  6161  ovmpt2ga  6162  sorpssuni  6490  sorpssint  6491  onoviun  6564  smo11  6585  omeulem1  6784  oeord  6790  oecan  6791  domss2  7225  mapxpen  7232  mapdom3  7238  fofinf1o  7346  elfir  7378  ordtype2  7459  wemapso2  7477  wdomima2g  7510  ixpiunwdom  7515  oemapvali  7596  cnfcom3clem  7618  tcrank  7764  fodomfi2  7897  cdaassen  8018  xpcdaen  8019  mapcdaen  8020  infcdaabs  8042  infdif  8045  ackbij1lem16  8071  cfeq0  8092  cfsuc  8093  isfin2-2  8155  fin23lem26  8161  domtriomlem  8278  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  zornn0g  8341  ttukey2g  8352  canthwe  8482  gchhar  8502  gchaleph  8506  gchaleph2  8507  wunpw  8538  tsktrss  8592  tskcard  8612  tskwun  8615  tskxp  8618  tskmap  8619  tskurn  8620  gruixp  8640  enqeq  8767  ltadd2  9133  readdcan  9196  subadd2  9265  nppcan  9280  nppcan3  9281  subsub2  9285  subsub4  9290  npncan3  9295  pnpcan  9296  pnncan  9298  subcan  9312  ltadd1  9451  leadd1  9452  leadd2  9453  ltsubadd  9454  ltsubadd2  9455  lesubadd  9456  lesubadd2  9457  lesub1  9478  lesub2  9479  ltsub1  9480  ltsub2  9481  mulcan  9615  mulcan2  9616  divmul  9637  divcan1  9643  diveq0  9644  divrec  9650  divass  9652  div23  9653  divdir  9657  divcan3  9658  div11  9660  diveq1  9664  divmuldiv  9670  divcan5  9672  redivcl  9689  div2neg  9693  ltmul1  9816  ltdiv1  9830  ledivmulOLD  9840  ledivmul2OLD  9844  lemuldiv  9845  lt2msq1  9849  ltdiv23  9857  lediv23  9858  infmrlb  9945  ofsubeq0  9953  ofnegsub  9954  ofsubge0  9955  zsupss  10521  suprzub  10523  rpgecl  10593  xrmaxlt  10725  xrltmin  10726  xrmaxle  10727  xrlemin  10728  xleadd1  10790  xltadd1  10791  xlemul1  10825  xlemul2  10826  xltmul1  10827  xadddir  10831  supxrre  10862  infmxrre  10870  ixxub  10893  icc0  10920  ubioc1  10921  ubicc2  10970  icoshftf1o  10976  snunioo  10979  snunico  10980  iccsplit  10985  fzm1  11082  flwordi  11174  flword2  11175  modcyc  11231  axdc4uzlem  11276  expgt1  11373  exprec  11376  expmulz  11381  leexp2a  11390  expubnd  11395  bernneq2  11461  expmulnbnd  11466  digit2  11467  swrdval  11719  ccatco  11759  s3cl  11796  swrds2  11835  shftuz  11839  cjdiv  11924  resqrcl  12014  absdiv  12055  caubnd  12117  limsuple  12227  limsuplt  12228  climuni  12301  iseraltlem3  12432  geoisum1c  12612  eflt  12673  dvdsval2  12810  dvdsadd2b  12847  dvdsexp  12860  dvdsgcdb  12999  mulgcd  13001  gcddiv  13004  mulgcddvds  13059  qredeq  13061  rpexp12i  13077  fermltl  13128  prmdiv  13129  odzcllem  13133  odzphi  13137  coprimeprodsq  13138  pythagtriplem6  13150  pythagtriplem7  13151  pythagtriplem13  13156  pceu  13175  pcgcd1  13205  vdwpc  13303  hashbcss  13327  ramval  13331  0ram2  13344  0ramcl  13346  isstruct2  13433  ressbas  13474  imasvscaval  13718  xpsadd  13756  xpsmul  13757  mrerintcl  13777  ismred2  13783  mremre  13784  mrieqv2d  13819  mreexmrid  13823  cofuass  14041  cofulid  14042  cofurid  14043  catcisolem  14216  posasymb  14364  ple1  14428  latleeqj1  14447  latleeqm1  14463  latnlemlt  14468  ipodrsfi  14544  mrelatglb  14565  mrelatlub  14567  imasmnd2  14687  imasmnd  14688  pwspjmhm  14722  frmdss2  14763  frmdup3  14766  grpinvadd  14822  grpsubeq0  14830  grppncan  14834  grpsubpropd2  14845  mulgnn0p1  14856  mulgnnsubcl  14857  mulgnn0subcl  14858  mulgsubcl  14859  mulgneg  14863  submmulg  14880  pwsinvg  14885  imasgrp2  14888  imasgrp  14889  subgcl  14909  subgsubcl  14910  subgsub  14911  subgmulg  14913  nsgconj  14928  cycsubg2cl  14933  nsgid  14941  ghmmulg  14973  ghmeqker  14987  odcong  15142  oddvds2  15157  odsubdvds  15160  pgpssslw  15203  slwn0  15204  sylow2blem1  15209  lsmssv  15232  lsmsubm  15242  lsmsubg  15243  subglsm  15260  lsmpropd  15264  pj1fval  15281  efgsval2  15320  frgp0  15347  frgpup3  15365  ablinvadd  15389  ablsub4  15392  ablpncan2  15395  subgabl  15410  cntzcmn  15414  gex2abl  15421  lsmsubg2  15429  prdscmnd  15431  ablfacrp  15579  rngidss  15645  rngcom  15647  gsumdixp  15670  imasrng  15680  unitmulcl  15724  unitmulclb  15725  dvrcan1  15751  dvrcan3  15752  irredrmul  15767  subrgmcl  15835  subrgdv  15840  cntzsubr  15855  isabvd  15863  islmod  15909  lmodcom  15945  lssvnegcl  15987  lssintcl  15995  lspss  16015  lspun  16018  lspsnvsi  16035  lmodvsinv  16067  lmodvsinv2  16068  0lmhm  16071  lmhmvsca  16076  reslmhm2  16084  lbsind2  16108  lsmsp  16113  lspsntri  16124  lsmcv  16168  lvecdim  16184  lbsextlem2  16186  lbsextg  16189  rrgeq0  16305  domneq0  16312  domnrrg  16315  aspss  16346  asclmul1  16353  asclmul2  16354  psrbagaddcl  16390  psrbagconcl  16393  psrgrp  16417  psrlmod  16420  psrrng  16429  psrcrng  16431  evlslem4  16519  psrplusgpropd  16584  psropprmul  16587  coe1add  16612  coe1mul2  16617  ply1tmcl  16619  coe1tm  16620  coe1tmfv1  16621  coe1sclmul  16629  coe1sclmul2  16631  chrcong  16765  zndvds  16785  ipeq0  16824  ip2eq  16839  cssmre  16875  obselocv  16910  clsndisj  17094  iscldtop  17114  lpss3  17163  restabs  17183  restcldi  17191  neitr  17198  restlp  17201  mnfnei  17239  lmconst  17279  cnrest2  17304  cnpresti  17306  hausnei2  17371  sshauslem  17390  cmpcld  17419  fiuncmp  17421  hauscmp  17424  concompclo  17451  2ndc1stc  17467  nllyrest  17502  kgen2ss  17540  xkopjcn  17641  xkococn  17645  cnmpt2t  17658  elqtop  17682  r0cld  17723  cmphaushmeo  17785  filss  17838  isfild  17843  fbasweak  17850  snfbas  17851  trfg  17876  trnei  17877  supfil  17880  ufinffr  17914  ufilen  17915  flimrest  17968  flimclslem  17969  lmflf  17990  fclsneii  18002  fclsrest  18009  cnpfcfi  18025  ptcmpg  18041  istgp2  18074  tgpconcompeqg  18094  prdstmdd  18106  tsmsxp  18137  ustssel  18188  ustn0  18203  ressusp  18248  cfiluweak  18278  neipcfilu  18279  psmetsym  18294  psmetge0  18296  xmetge0  18327  xmetsym  18330  blvalps  18368  blval  18369  xblcntrps  18393  xblcntr  18394  xmssym  18448  blsscls2  18487  stdbdxmet  18498  prdsxms  18513  prdsms  18514  metustblOLD  18563  metustbl  18564  restmetu  18570  isngp4  18611  nmmtri  18621  nmsub  18622  nmrtri  18623  nmtri  18625  nlmmul0or  18672  nmods  18731  xrsmopn  18796  iccntr  18805  metds0  18833  cncfmptc  18894  iirev  18907  icoopnst  18917  iocopnst  18918  icchmeo  18919  iccpnfhmeo  18923  pi1grplem  19027  pi1xfr  19033  isclmi  19055  cphreccllem  19094  ipcau  19148  nmpar  19150  fmcfil  19178  iscau2  19183  cfilres  19202  caussi  19203  caublcls  19214  bcthlem5  19234  srabn  19267  rlmbn  19268  pjth  19293  pjth2  19294  cniccbdd  19311  ovolgelb  19329  ovollecl  19332  ovolunnul  19349  ovolicc  19372  cmmbl  19382  iundisj2  19396  voliunlem2  19398  voliunlem3  19399  ovolioo  19415  volcn  19451  cncombf  19503  itg1le  19558  itg2lecl  19583  itgconst  19663  bddibl  19684  dvfval  19737  dvid  19757  dvcnp  19758  dvcnp2  19759  dvnf  19766  dvnbss  19767  dvn2bss  19769  evlsval2  19894  mdegldg  19942  deg1lt  19973  deg1mul3  19991  deg1mul3le  19992  q1peqb  20030  r1pcl  20033  r1pdeglt  20034  r1pid  20035  dvdsr1p  20037  fta1b  20045  drnguc1p  20046  ig1peu  20047  elplyr  20073  dgrub  20106  dgrlb  20108  dgradd2  20139  ofmulrt  20152  quotcl2  20172  quotdgr  20173  quotcan  20179  vieta1  20182  aannenlem1  20198  aannenlem2  20199  aalioulem3  20204  aaliou2  20210  ulmcl  20250  tanord1  20392  tanord  20393  cxpef  20509  cxpadd  20523  cxpneg  20525  cxpsub  20526  divcxp  20531  cxpmul  20532  cxpeq  20594  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  ang180lem4  20607  angpieqvd  20625  xrlimcnp  20760  cxp2lim  20768  wilthlem3  20806  chtwordi  20892  ppiwordi  20898  sgmppw  20934  dchrabl  20991  bcmono  21014  efexple  21018  lgsneg1  21057  lgsmod  21058  lgssq  21072  lgsdirnn0  21076  lgsdinn0  21077  lgsqrlem5  21082  lgsquad  21094  dirith  21176  pntrmax  21211  abvcxp  21262  cusgra3v  21426  2trllemE  21506  1pthon  21544  2pthon  21555  grpoasscan2  21779  grpoinvop  21782  grpopncan  21792  grponpcan  21793  gxcom  21810  gxinv  21811  gxsuc  21813  gxdi  21837  rngodi  21926  rngosn  21945  zerdivemp1  21975  nvpncan2  22090  nvnncan  22097  nvs  22104  nvdif  22107  nvpi  22108  nvabs  22115  nv1  22118  lno0  22210  lnocoi  22211  nmooge0  22221  shlub  22869  pjspansn  23032  adj2  23390  kbmul  23411  adjlnop  23542  cdj3lem3a  23895  iundisj2f  23983  curry2ima  24050  snunioc  24090  iocinioc2  24095  iundisj2fi  24106  divnumden2  24114  xreceu  24121  xdivcl  24123  xdivmul  24124  xdivrec  24126  ress0g  24135  tleile  24142  xrsmulgzz  24153  xrge0addass  24164  xrge0neqmnf  24165  cnre2csqlem  24261  nmmulg  24305  qqhval2lem  24318  relogbcl  24355  logb1  24356  logblt  24359  ind1  24369  esummulc1  24424  hasheuni  24428  sigaclcu  24453  difelsiga  24469  elsigagen2  24484  sigagenss2  24486  isrnmeas  24507  measvun  24516  measvunilem  24519  measvunilem0  24520  measvuni  24521  measres  24529  aean  24548  mbfmco2  24568  dya2icoseg2  24581  sitgclg  24609  totprob  24638  probmeasb  24641  cndprobval  24644  cndprobnul  24648  cndprobprob  24649  bayesth  24650  orvclteinc  24686  lgamgulmlem1  24766  cvmcov2  24915  dedekind  25140  dedekindle  25141  subdivcomb2  25149  binomrisefac  25309  trpredpo  25452  elno2  25522  brbtwn2  25748  colinearalglem1  25749  colinearalglem2  25750  axcgrid  25759  ax5seglem2  25772  axbtwnid  25782  axpasch  25784  axcontlem4  25810  axcontlem8  25814  cgrrflx  25825  cgrtriv  25840  btwntriv2  25850  btwntriv1  25854  trisegint  25866  btwnxfr  25894  colineardim1  25899  colineartriv1  25905  colineartriv2  25906  btwnconn1lem7  25931  segcon2  25943  seglerflx  25950  outsidene2  25962  liness  25983  hilbert1.1  25992  bpolycl  26002  areacirclem4  26183  areacirclem6  26186  areacirc  26187  comppfsc  26277  mettrifi  26353  cnresima  26363  ismtybndlem  26405  rrnmval  26427  zerdivemp1x  26461  isfldidl  26568  ismrcd1  26642  istopclsd  26644  ismrc  26645  mapfzcons  26662  mzpcl34  26678  mzpexpmpt  26692  mzpsubst  26695  eldioph  26706  diophrw  26707  pellexlem5  26786  pellex  26788  pell14qrgap  26828  pellfundlb  26837  pellfundglb  26838  pellfundex  26839  rmxycomplete  26870  rmxyadd  26874  monotoddzz  26896  rmxypos  26902  rmygeid  26919  acongrep  26935  acongeq  26938  coprmdvdsb  26942  modabsdifz  26946  dvdsabsmod0  26947  jm2.22  26956  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  rpnnen3lem  26992  pwssplit0  27055  pwssplit1  27056  pwssplit2  27057  pwssplit3  27058  pwssplit4  27059  dsmmsubg  27077  uvcresum  27110  frlmsplit2  27111  frlmsslss  27112  frlmup4  27121  isnumbasgrplem2  27137  islindf2  27152  lindfind2  27156  hbtlem2  27196  mpaaeu  27223  pmtrmvd  27266  pmtrfrn  27268  pmtrfb  27274  psgnunilem4  27288  matrng  27348  idomrootle  27379  fiuneneq  27381  proot1hash  27387  ofdivrec  27411  ofdivcan4  27412  ubelsupr  27558  fmul01  27577  fmuldfeq  27580  fmul01lt1lem2  27582  fmul01lt1  27583  climsuse  27601  stoweidlem3  27619  stoweidlem6  27622  stoweidlem8  27624  stoweidlem10  27626  stoweidlem19  27635  stoweidlem26  27642  stoweidlem28  27644  stoweidlem31  27647  stoweidlem57  27673  stoweidlem59  27675  stoweidlem60  27676  wallispilem3  27683  stirlinglem13  27702  sigaraf  27710  sigarmf  27711  sigaras  27712  sigarms  27713  sigarls  27714  sigarexp  27716  sigarperm  27717  sigarcol  27721  ssfzo12  27990  swrd0swrd  28009  usgra2wlkspth  28038  el2wlkonotot0  28069  vdn0frgrav2  28128  vdn1frgrav2  28130  3orbi123  28305  alrim3con13v  28328  3orbi123VD  28671  19.21a3con13vVD  28673  tratrbVD  28682  bnj906  29007  bnj1110  29057  bnj1128  29065  bnj1145  29068  bnj1189  29084  bnj1204  29087  bnj1279  29093  bnj1311  29099  bnj1408  29111  toycom  29455  lshpnelb  29467  lsatfixedN  29492  lssatomic  29494  lcvat  29513  lsatcveq0  29515  lcvexchlem4  29520  lcvexchlem5  29521  lsatcvatlem  29532  islshpcv  29536  l1cvpat  29537  lfladd  29549  lflsub  29550  lflmul  29551  lfl1  29553  eqlkr  29582  lkrshp  29588  lshpsmreu  29592  lshpkrex  29601  ldualgrplem  29628  lduallmodlem  29635  lkrlspeqN  29654  oldmm1  29700  olj01  29708  omllaw4  29729  omllaw5N  29730  cmt2N  29733  cmt3N  29734  cmtbr2N  29736  cmtbr3N  29737  cmtbr4N  29738  lecmtN  29739  meetat  29779  atn0  29791  cvlcvr1  29822  cvlcvrp  29823  cvlsupr6  29830  hlrelat2  29885  exatleN  29886  cvr2N  29893  hlrelat3  29894  cvrval3  29895  cvrval4N  29896  cvrval5  29897  cvrexch  29902  lnnat  29909  atle  29918  atlt  29919  2atlt  29921  atbtwnexOLDN  29929  atbtwnex  29930  1cvratlt  29956  ps-2b  29964  3atlem5  29969  llnnleat  29995  llnle  30000  llnexatN  30003  llncmp  30004  2llnmat  30006  lplni2  30019  lvolex3N  30020  lplnle  30022  lplnnleat  30024  lplncmp  30044  lplnexatN  30045  2atnelvolN  30069  4atlem10  30088  4atlem11  30091  4atlem12  30094  lvolcmp  30099  dalemswapyz  30138  dalemswapyzps  30172  dalem56  30210  pmaple  30243  lneq2at  30260  lnjatN  30262  lncmp  30265  2lnat  30266  elpadd2at  30288  pmapjat1  30335  pmapjat2  30336  dalawlem10  30362  dalawlem13  30365  dalawlem15  30367  dalaw  30368  elpcliN  30375  pclunN  30380  polcon3N  30399  paddunN  30409  poldmj1N  30410  pmapj2N  30411  osumcllem5N  30442  osumcllem7N  30444  osumcllem10N  30447  lhp0lt  30485  lhpexle1  30490  lhpexle2lem  30491  lhpexle3lem  30493  lhpj1  30504  lhpmcvr5N  30509  lhpat4N  30526  4atexlem7  30557  4atex3  30563  ldilcnv  30597  ldilco  30598  ltrnatb  30619  ltrnel  30621  ltrncnvel  30624  ltrn11at  30629  ltrnmw  30633  trlval2  30645  trljat2  30649  trlat  30651  trl0  30652  trlnidat  30655  trlnidatb  30659  trlval3  30669  cdlemc1  30673  cdlemc2  30674  cdlemd8  30687  cdlemd9  30688  cdleme0ex2N  30706  cdleme7b  30726  cdleme7d  30728  cdleme10  30736  cdleme11dN  30744  cdleme11e  30745  cdleme21h  30816  cdleme26ee  30842  cdlemefr29bpre0N  30888  cdlemefr29clN  30889  cdlemefr32fvaN  30891  cdlemefr32fva1  30892  cdlemefs29bpre0N  30898  cdlemefs29bpre1N  30899  cdlemefs29cpre1N  30900  cdlemefs29clN  30901  cdlemefs32fvaN  30904  cdlemefs32fva1  30905  cdleme32fva  30919  cdleme32fvaw  30921  cdleme32le  30929  cdleme38m  30945  cdleme39a  30947  cdleme17d3  30978  cdlemeg49le  30993  cdlemeg46fvaw  30998  cdlemf1  31043  cdlemfnid  31046  cdlemg2ce  31074  cdlemb3  31088  cdlemg7fvbwN  31089  cdlemg4b1  31091  cdlemg7aN  31107  cdlemg10bALTN  31118  cdlemg12b  31126  cdlemg12d  31128  cdlemg12f  31130  cdlemg12g  31131  cdlemg13  31134  cdlemg31c  31181  cdlemg34  31194  cdlemg36  31196  trlcone  31210  cdlemg44  31215  cdlemg48  31219  tendococl  31254  tendoicl  31278  tendocan  31306  cdlemk7  31330  cdlemk12  31332  cdlemk12u  31354  cdlemk26b-3  31387  cdlemk26-3  31388  cdlemk11ta  31411  cdlemk19ylem  31412  cdlemkid3N  31415  cdlemk11tc  31427  cdlemk11t  31428  cdlemk45  31429  cdlemk46  31430  cdlemk49  31433  cdlemk54  31440  cdlemk55b  31442  cdlemk56  31453  cdlemk19w  31454  cdleml3N  31460  cdleml4N  31461  cdleml6  31463  cdleml7  31464  cdleml8  31465  erngdvlem4-rN  31481  tendocnv  31504  tendospcanN  31506  dia2dimlem12  31558  tendoinvcl  31587  tendolinv  31588  tendorinv  31589  dvhopellsm  31600  dicvaddcl  31673  dicvscacl  31674  cdlemn3  31680  cdlemn4  31681  cdlemn4a  31682  dihord2cN  31704  dihord11c  31707  dih1dimb2  31724  dihvalcq2  31730  dihord5b  31742  dihord5apre  31745  dihglblem2N  31777  dihjatc1  31794  dihmeetlem20N  31809  dihmeetALTN  31810  dih1dimatlem0  31811  dihatexv  31821  dochss  31848  dochdmj1  31873  dvh4dimlem  31926  dvh3dim3N  31932  dochsatshpb  31935  dochexmidlem4  31946  dochexmidlem5  31947  dochexmidlem8  31950  dochkr1  31961  dochkr1OLDN  31962  lcfl7lem  31982  lcfl8  31985  lcfrlem16  32041  lcfrlem40  32065  mapdval2N  32113  mapdpglem24  32187  mapdh6iN  32227  mapdh8ad  32262  mapdh8e  32267  hdmap1fval  32280  hdmap1l6i  32302  hdmapfval  32313  hdmapval0  32319  hdmapevec  32321  hdmapval3N  32324  hdmap10lem  32325  hdmap11lem2  32328  hdmaprnlem15N  32347  hdmaprnlem16N  32348  hdmap14lem10  32363  hdmap14lem11  32364  hdmap14lem12  32365  hgmapfval  32372  hgmapval1  32379  hgmapadd  32380  hgmapmul  32381  hgmaprnlem3N  32384  hgmaprnlem4N  32385  hgmap11  32388  hlhilsrnglem  32439  hlhilphllem  32445
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