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

Theorem simprbi 451
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simprbi.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simprbi  |-  ( ph  ->  ch )

Proof of Theorem simprbi
StepHypRef Expression
1 simprbi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpi 187 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 450 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  sb1  1658  eumo  2279  2eu1  2319  reurmo  2867  pssne  3387  pssn2lp  3392  ssnpss  3394  eldifn  3414  rabsnt  3825  eldifsni  3872  unimax  3992  ssintub  4011  moop2  4393  pwssun  4431  weso  4515  ordwe  4536  reusv6OLD  4675  onminesb  4719  onminsb  4720  tfis  4775  limomss  4791  nnlim  4799  ssnlim  4804  opelxp2  4853  funmo  5411  funopg  5426  funun  5436  fununi  5458  funimaexg  5471  fndm  5485  frn  5538  f1ss  5585  f1ssr  5586  f1ssres  5587  forn  5597  f1f1orn  5626  f1orescnv  5631  f1imacnv  5632  funcocnv2  5641  dffv2  5736  exfo  5827  foelrn  5828  isorel  5986  isoini2  5999  fovcl  6115  f1opw  6239  curry1  6378  curry2  6381  fnwelem  6398  mpt2xopn0yelv  6401  f1ofveu  6521  tz7.48lem  6635  dif20el  6686  oeordi  6767  oeeulem  6781  oeeui  6782  nnawordex  6817  swoer  6870  erdisj  6889  eceqoveq  6946  mapsnconst  6996  ixpn0  7031  resixpfo  7037  boxcutc  7042  sdomnen  7073  en0  7107  en1  7111  domunsncan  7145  fodomr  7195  phplem4  7226  php3  7230  unxpdomlem3  7252  fineqvlem  7260  suppfif1  7336  f1opwfi  7346  supub  7398  suplub  7399  ordtypelem2  7422  ordtypelem3  7423  ordtypelem6  7426  ordtypelem7  7427  wemapso2  7455  wdom2d  7482  brwdom3  7484  ixpiunwdom  7493  inf3lem2  7518  inf3lem6  7522  oancom  7540  infdifsn  7545  cantnfp1lem3  7570  cantnflem3  7581  cantnflem4  7582  cantnf  7583  mapfien  7587  oef1o  7589  cnfcomlem  7590  cnfcom3  7595  tctr  7613  tz9.12lem3  7649  scottex  7743  cardid2  7774  infxpenlem  7829  acni3  7862  cardaleph  7904  iscard3  7908  dfac5lem4  7941  dfac5lem5  7942  kmlem1  7964  cofsmo  8083  fin4en1  8123  enfin2i  8135  fin23lem28  8154  fin23lem38  8163  isf32lem6  8172  enfin1ai  8198  isfin1-3  8200  hsmexlem2  8241  hsmexlem4  8243  domtriomlem  8256  axdc2lem  8262  axdc3lem2  8265  ac6num  8293  zorn2lem2  8311  brdom3  8340  alephval2  8381  alephreg  8391  pwcfsdom  8392  smobeth  8395  fpwwe2lem6  8444  fpwwe2lem13  8451  canthp1lem2  8462  pwfseqlem3  8469  hargch  8486  winalim2  8505  gchina  8508  inar1  8584  0npi  8693  mulclpi  8704  mulcanpi  8711  nlt1pi  8717  nqereu  8740  prcdnq  8804  prnmax  8806  ltresr2  8950  axrnegex  8971  axpre-sup  8978  1nuz2  10484  zsupss  10498  rpgt0  10556  ixxss1  10867  ixxss2  10868  ixxss12  10869  lbioo  10880  ubioo  10881  iccss2  10914  iccssico2  10917  elfzuz3  10989  uzdisj  11050  serge0  11305  expge0  11344  expge1  11345  expaddzlem  11351  hashfun  11628  shftfn  11816  sqrlem6  11981  rlimss  12224  lo1dm  12241  o1dm  12252  rlimrege0  12301  fsumf1o  12445  fsumge0  12502  incexc2  12546  supcvg  12563  divalglem9  12849  bitsfzolem  12874  bitsinv2  12883  bitsf1ocnv  12884  bitsf1  12886  gcdcllem1  12939  bezout  12970  prmind2  13018  nprm  13021  sqnprm  13026  dvdsprm  13027  coprm  13028  isprm5  13040  prmexpb  13045  phibndlem  13087  dfphi2  13091  phimullem  13096  pclem  13140  pcpre1  13144  pcidlem  13173  pcmpt  13189  expnprm  13199  prmreclem1  13212  prmreclem2  13213  prmreclem5  13216  1arith  13223  4sqlem18  13258  vdwnnlem3  13293  ramtlecl  13296  rami  13311  0ram  13316  ramub1lem1  13322  firest  13588  acsfiel  13807  isacs1i  13810  catlid  13836  catrid  13837  fullfo  14037  fthf1  14042  fthoppc  14048  invfuc  14099  prslem  14316  posi  14335  latlem  14405  clatlem  14467  dlatmjdi  14548  pslem  14566  tsrlin  14579  cnvtsr  14582  tsrdir  14611  mndid  14625  mhmf  14671  mhmlin  14673  mhm0  14674  grpinvex  14748  grplinv  14779  mulgz  14839  mulgdirlem  14842  mulgdir  14843  mulgass  14848  nsgbi  14899  nmzbi  14908  ghmf  14938  ghmlin  14939  conjnsg  14969  gimf1o  14978  gagrpid  14999  gaf  15000  gaass  15002  odid  15104  odf1o2  15135  gexid  15143  sylow1lem4  15163  odcau  15166  pj1id  15259  efgredeu  15312  ablcmn  15346  cmncom  15356  mulgdi  15377  gexexlem  15395  torsubg  15397  cyggenod2  15423  cygctb  15429  ghmcyg  15433  dprdf1o  15518  dprd2dlem1  15527  dprd2da  15528  ablfacrplem  15551  ablfaclem2  15572  ablfac2  15575  crngmgp  15600  rhmmhm  15753  rhmghm  15754  drngunit  15768  drngmgp  15775  drngid  15777  subrgss  15797  subrg1cl  15804  issubdrg  15821  abvge0  15841  srngcnv  15869  lmhmlin  16039  lmimf1o  16063  lvecdrng  16105  lspsolvlem  16142  islbs3  16155  lbsextlem3  16160  2idlcpbl  16233  nzrnz  16259  opprnzr  16263  rrgeq0i  16277  domneq0  16285  domnrrg  16288  drngdomn  16291  fldidom  16293  assalem  16304  mplsubrglem  16430  mplcoe1  16456  mplbas2  16459  opsrtoslem2  16473  mplelsfi  16479  coe1mul2  16590  zrngunit  16689  prmirredlem  16697  znidomb  16766  cygzn  16775  pjf  16864  toponuni  16916  tpsuni  16927  clsval2  17038  mretopd  17080  neips  17101  neiptoptop  17119  neiptopnei  17120  perflp  17141  perfi  17142  restfpw  17166  cnf  17233  cnpf  17234  cnpimaex  17243  cnima  17252  t0sep  17311  t1sncld  17313  t1ficld  17314  hausnei  17315  regsep  17321  pnrmcld  17329  nrmsep3  17342  cnrmi  17347  cmpcov  17375  discmp  17384  tgcmp  17387  uncmp  17389  hauscmplem  17392  cmpfi  17394  conclo  17400  1stcclb  17429  2ndcdisj  17441  llyi  17459  nllyi  17460  ptpjpre1  17525  ptpjcn  17565  ptpjopn  17566  ptclsg  17569  dfac14  17572  txdis1cn  17589  pthaus  17592  hauseqlcld  17600  txkgen  17606  xkococn  17614  txcon  17643  hmeocnvcn  17715  fbssfi  17791  filss  17807  ufilss  17859  uffixfr  17877  flimneiss  17920  flimelbas  17922  fclscf  17979  flimfnfcls  17982  alexsublem  17997  alexsubb  17999  alexsubALT  18004  ptcmplem2  18006  ptcmplem3  18007  ptcmplem4  18008  tmdgsum2  18048  ghmcnp  18066  tgpt0  18070  divstgplem  18072  tsmsfbas  18079  tsmslem1  18080  tsmsgsum  18090  tsmssubm  18094  tsmsres  18095  tsmsf1o  18096  tsmsmhm  18097  tsmsadd  18098  tsmsxplem1  18104  tsmsxplem2  18105  tsmsxp  18106  istdrg2  18129  vscacn  18137  tvctdrg  18144  uspreg  18226  ucncn  18237  neipcfilu  18248  cuspcvg  18253  isxmet2d  18267  prdsxmetlem  18307  imasdsf1olem  18312  xmstopn  18372  mstopn  18373  stdbdxmet  18436  prdsxmslem2  18450  nrgabv  18569  nmvs  18584  nvclvec  18604  nmoge0  18627  nghmcl  18633  nmoi  18634  nghmghm  18640  nmhmlmhm  18655  nmhmnghm  18656  icccmp  18728  xrge0gsumle  18736  xrge0tsms  18737  metds0  18752  metdstri  18753  metdsre  18755  metdseq0  18756  metdscnlem  18757  metnrmlem1a  18760  icopnfcnv  18839  xrhmeo  18843  pcoval1  18910  cphreccllem  19013  cmetcvg  19110  lmle  19126  cmscmet  19169  cmetcusp1  19175  hlcph  19186  minveclem4  19201  ivthlem3  19218  ovolmge0  19241  ovolicc1  19280  ovolicc2lem3  19283  ovolicc2lem5  19285  mblsplit  19296  dyadmbl  19360  mbfdm  19388  mbfadd  19421  mbfsub  19422  i1ff  19436  i1frn  19437  i1fima2  19439  mbfmul  19486  itg2monolem1  19510  bddmulibl  19598  dvnres  19685  c1liplem1  19748  c1lip2  19750  dvge0  19758  lhop1lem  19765  itgsubstlem  19800  fta1glem1  19956  fta1glem2  19957  fta1b  19960  plyf  19985  plypf1  19999  plyadd  20004  plymul  20005  coeeu  20012  dgrlem  20016  coeid  20025  elqaalem3  20106  aareccl  20111  eff1olem  20318  relogf1o  20332  logdmn0  20399  logcnlem2  20402  logcnlem3  20403  dvloglem  20407  efopnlem1  20415  efopnlem2  20416  logtayl2  20421  cxpcn3lem  20499  cxpcn3  20500  atandmneg  20614  atandmcj  20617  efiatan2  20625  cosatan  20629  cosatanne0  20630  dvatan  20643  areage0  20670  cxp2lim  20683  jensenlem2  20694  jensen  20695  wilthlem1  20719  wilth  20722  ftalem3  20725  efnnfsumcl  20753  isppw  20765  efchtdvds  20810  sqff1o  20833  dvdsdivcl  20834  fsumdvdsdiaglem  20836  dvdsppwf1o  20839  dvdsflf1o  20840  musum  20844  muinv  20846  dvdsmulf1o  20847  fsumvma2  20866  vmasum  20868  chpval2  20870  chpchtsum  20871  chpub  20872  mersenne  20879  perfect1  20880  bposlem1  20936  bposlem5  20940  bposlem6  20941  lgsfle1  20957  lgsle1  20963  lgsdirprm  20981  lgsne0  20985  lgsqrlem4  20996  lgseisenlem3  21003  lgseisenlem4  21004  lgsquadlem1  21006  lgsquadlem2  21007  2sqblem  21029  chebbnd1lem1  21031  chebbnd1  21034  chtppilim  21037  chpchtlim  21041  chpo1ub  21042  rplogsumlem2  21047  rpvmasumlem  21049  dchrmusumlema  21055  dchrvmasumlem1  21057  dchrisum0flblem2  21071  dchrisum0lema  21076  dchrisum0lem2a  21079  logsqvma  21104  selberg3lem2  21120  pntrsumo1  21127  pnt2  21175  ostthlem1  21189  padicabvf  21193  ostth3  21200  umgrale  21224  usgraedg2  21263  eupatrl  21539  gxneg  21703  gxadd  21712  gxmul  21715  ablocom  21722  subgoablo  21748  smgrpisass  21770  mndoisexid  21777  zrdivrng  21869  phpar2  22173  cbncms  22216  hlph  22240  hcaucvg  22537  hlimconvi  22542  shaddcl  22568  shmulcl  22569  shmulclOLD  22570  chlimi  22586  chcompl  22594  choc1  22678  nmopre  23222  cnopc  23265  lnopl  23266  unop  23267  hmop  23274  cnfnc  23282  lnfnl  23283  nlelshi  23412  cnlnadjlem5  23423  elpjidm  23536  mdslle1i  23669  mdslle2i  23670  atcv0  23694  chpssati  23715  fovcld  23894  ssnnssfz  23985  resspos  24027  resstos  24028  xrge0tsmsd  24053  ofldaddlt  24068  ofld0le1  24069  subofld  24072  kerf1hrm  24079  tpr2rico  24115  rge0scvg  24140  zrhunitpreima  24162  qqhrhm  24173  esummono  24247  gsumesum  24248  esumpinfval  24260  esumpcvgval  24265  esumpmono  24266  0elsiga  24294  sigaclcu  24297  issgon  24303  sxuni  24344  isrnmeas  24351  measvuni  24363  measssd  24364  imambfm  24407  elmbfmvol2  24412  dya2icoseg2  24423  probtot  24450  ballotlem4  24536  ballotlem5  24537  ballotlemfrc  24564  ballotlemirc  24569  ballotth  24575  eldmgm  24586  dmgmaddn0  24587  dmlogdmgm  24588  lgamgulmlem2  24594  lgamgulmlem3  24595  lgamgulmlem5  24597  lgambdd  24601  lgamucov  24602  subfacp1lem3  24648  subfacp1lem5  24650  pconcn  24691  sconpht  24696  conpcon  24702  cvmcov  24730  cvmliftlem1  24752  cvmliftlem10  24761  cvmlift2lem11  24780  cvmlift2lem12  24781  fprodf1o  25052  fundmpss  25147  tfisg  25229  wfisg  25234  frinsg  25270  wfrlem5  25285  frrlem5  25310  sltval2  25335  txpss3v  25443  pprodss4v  25449  axcontlem7  25624  axcontlem10  25627  onint1  25914  itg2gt0cn  25961  fnetg  26046  refssfne  26066  neibastop1  26080  filnetlem3  26101  cover2  26107  indexa  26127  istotbnd3  26172  sstotbnd2  26175  sstotbnd  26176  totbndss  26178  equivtotbnd  26179  isbnd3  26185  totbndbnd  26190  equivbnd  26191  prdsbnd  26194  prdstotbnd  26195  heibor  26222  crngocom  26303  isfld2  26307  dmncrng  26358  prter2  26422  nacsfg  26451  nacsfix  26458  mzpindd  26495  diophrw  26509  diophrex  26526  rexzrexnn0  26556  pell1234qrdich  26616  rmspecnonsq  26662  rmspecfund  26664  rmspecpos  26671  monotoddzzfi  26697  ltrmxnn0  26706  rmxnn  26708  jm2.23  26759  jm3.1lem2  26781  dnnumch3  26814  lnmlssfg  26848  lnmlmic  26856  frlmsslsp  26918  frlmlbs  26919  f1lindf  26962  lnrlnm  26987  lnr2i  26990  lpirlnr  26991  hbtlem6  27003  hbt  27004  mnccoe  27013  psgnunilem5  27087  cntzsdrg  27180  idomrootle  27181  proot1mul  27185  phisum  27188  proot1hash  27189  deg1mhm  27196  stoweidlem7  27425  stoweidlem14  27432  stoweidlem16  27434  stoweidlem24  27442  stoweidlem31  27449  stoweidlem39  27457  stoweidlem50  27468  stoweidlem54  27472  stoweidlem57  27475  wallispilem3  27485  2reu1  27633  nfunsnafv  27676  faovcl  27734  ordelordALT  27966  2uasbanh  27992  ordelordALTVD  28321  bnj642  28455  bnj643  28456  bnj645  28457  bnj707  28462  bnj1379  28541  bnj1538  28565  bnj110  28568  bnj93  28573  bnj906  28640  bnj1006  28669  bnj1110  28690  bnj1121  28693  bnj1172  28709  bnj1204  28720  bnj1321  28735  bnj1364  28736  bnj1398  28742  bnj1450  28758  bnj1312  28766  bnj1501  28775  bnj1523  28779  toycom  29088  lsateln0  29111  lpssat  29129  lssat  29132  oposlem  29299  olop  29330  omllaw  29359  cvlexch1  29444  dihpN  31452  mapdordlem2  31753
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
  Copyright terms: Public domain W3C validator