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  1659  eumo  2294  2eu1  2334  reurmo  2883  pssne  3403  pssn2lp  3408  ssnpss  3410  eldifn  3430  rabsnt  3841  eldifsni  3888  unimax  4009  ssintub  4028  moop2  4411  pwssun  4449  weso  4533  ordwe  4554  reusv6OLD  4693  onminesb  4737  onminsb  4738  tfis  4793  limomss  4809  nnlim  4817  ssnlim  4822  opelxp2  4871  funmo  5429  funopg  5444  funun  5454  fununi  5476  funimaexg  5489  fndm  5503  frn  5556  f1ss  5603  f1ssr  5604  f1ssres  5605  forn  5615  f1f1orn  5644  f1orescnv  5649  f1imacnv  5650  funcocnv2  5659  dffv2  5755  exfo  5846  foelrn  5847  isorel  6005  isoini2  6018  fovcl  6134  f1opw  6258  curry1  6397  curry2  6400  f1o2ndf1  6413  fnwelem  6420  mpt2xopn0yelv  6423  f1ofveu  6543  tz7.48lem  6657  dif20el  6708  oeordi  6789  oeeulem  6803  oeeui  6804  nnawordex  6839  swoer  6892  erdisj  6911  eceqoveq  6968  mapsnconst  7018  ixpn0  7053  resixpfo  7059  boxcutc  7064  sdomnen  7095  en0  7129  en1  7133  domunsncan  7167  fodomr  7217  phplem4  7248  php3  7252  unxpdomlem3  7274  fineqvlem  7282  suppfif1  7358  f1opwfi  7368  supub  7420  suplub  7421  ordtypelem2  7444  ordtypelem3  7445  ordtypelem6  7448  ordtypelem7  7449  wemapso2  7477  wdom2d  7504  brwdom3  7506  ixpiunwdom  7515  inf3lem2  7540  inf3lem6  7544  oancom  7562  infdifsn  7567  cantnfp1lem3  7592  cantnflem3  7603  cantnflem4  7604  cantnf  7605  mapfien  7609  oef1o  7611  cnfcomlem  7612  cnfcom3  7617  tctr  7635  tz9.12lem3  7671  scottex  7765  cardid2  7796  infxpenlem  7851  acni3  7884  cardaleph  7926  iscard3  7930  dfac5lem4  7963  dfac5lem5  7964  kmlem1  7986  cofsmo  8105  fin4en1  8145  enfin2i  8157  fin23lem28  8176  fin23lem38  8185  isf32lem6  8194  enfin1ai  8220  isfin1-3  8222  hsmexlem2  8263  hsmexlem4  8265  domtriomlem  8278  axdc2lem  8284  axdc3lem2  8287  ac6num  8315  zorn2lem2  8333  brdom3  8362  alephval2  8403  alephreg  8413  pwcfsdom  8414  smobeth  8417  fpwwe2lem6  8466  fpwwe2lem13  8473  canthp1lem2  8484  pwfseqlem3  8491  hargch  8508  winalim2  8527  gchina  8530  inar1  8606  0npi  8715  mulclpi  8726  mulcanpi  8733  nlt1pi  8739  nqereu  8762  prcdnq  8826  prnmax  8828  ltresr2  8972  axrnegex  8993  axpre-sup  9000  1nuz2  10507  zsupss  10521  rpgt0  10579  ixxss1  10890  ixxss2  10891  ixxss12  10892  lbioo  10903  ubioo  10904  iccss2  10937  iccssico2  10940  elfzuz3  11012  uzdisj  11074  serge0  11332  expge0  11371  expge1  11372  expaddzlem  11378  hashfun  11655  shftfn  11843  sqrlem6  12008  rlimss  12251  lo1dm  12268  o1dm  12279  rlimrege0  12328  fsumf1o  12472  fsumge0  12529  incexc2  12573  supcvg  12590  divalglem9  12876  bitsfzolem  12901  bitsinv2  12910  bitsf1ocnv  12911  bitsf1  12913  gcdcllem1  12966  bezout  12997  prmind2  13045  nprm  13048  sqnprm  13053  dvdsprm  13054  coprm  13055  isprm5  13067  prmexpb  13072  phibndlem  13114  dfphi2  13118  phimullem  13123  pclem  13167  pcpre1  13171  pcidlem  13200  pcmpt  13216  expnprm  13226  prmreclem1  13239  prmreclem2  13240  prmreclem5  13243  1arith  13250  4sqlem18  13285  vdwnnlem3  13320  ramtlecl  13323  rami  13338  0ram  13343  ramub1lem1  13349  firest  13615  acsfiel  13834  isacs1i  13837  catlid  13863  catrid  13864  fullfo  14064  fthf1  14069  fthoppc  14075  invfuc  14126  prslem  14343  posi  14362  latlem  14432  clatlem  14494  dlatmjdi  14575  pslem  14593  tsrlin  14606  cnvtsr  14609  tsrdir  14638  mndid  14652  mhmf  14698  mhmlin  14700  mhm0  14701  grpinvex  14775  grplinv  14806  mulgz  14866  mulgdirlem  14869  mulgdir  14870  mulgass  14875  nsgbi  14926  nmzbi  14935  ghmf  14965  ghmlin  14966  conjnsg  14996  gimf1o  15005  gagrpid  15026  gaf  15027  gaass  15029  odid  15131  odf1o2  15162  gexid  15170  sylow1lem4  15190  odcau  15193  pj1id  15286  efgredeu  15339  ablcmn  15373  cmncom  15383  mulgdi  15404  gexexlem  15422  torsubg  15424  cyggenod2  15450  cygctb  15456  ghmcyg  15460  dprdf1o  15545  dprd2dlem1  15554  dprd2da  15555  ablfacrplem  15578  ablfaclem2  15599  ablfac2  15602  crngmgp  15627  rhmmhm  15780  rhmghm  15781  drngunit  15795  drngmgp  15802  drngid  15804  subrgss  15824  subrg1cl  15831  issubdrg  15848  abvge0  15868  srngcnv  15896  lmhmlin  16066  lmimf1o  16090  lvecdrng  16132  lspsolvlem  16169  islbs3  16182  lbsextlem3  16187  2idlcpbl  16260  nzrnz  16286  opprnzr  16290  rrgeq0i  16304  domneq0  16312  domnrrg  16315  drngdomn  16318  fldidom  16320  assalem  16331  mplsubrglem  16457  mplcoe1  16483  mplbas2  16486  opsrtoslem2  16500  mplelsfi  16506  coe1mul2  16617  zrngunit  16720  prmirredlem  16728  znidomb  16797  cygzn  16806  pjf  16895  toponuni  16947  tpsuni  16958  clsval2  17069  mretopd  17111  neips  17132  neiptoptop  17150  neiptopnei  17151  perflp  17172  perfi  17173  restfpw  17197  cnf  17264  cnpf  17265  cnpimaex  17274  cnima  17283  t0sep  17342  t1sncld  17344  t1ficld  17345  hausnei  17346  regsep  17352  pnrmcld  17360  nrmsep3  17373  cnrmi  17378  cmpcov  17406  discmp  17415  tgcmp  17418  uncmp  17420  hauscmplem  17423  cmpfi  17425  conclo  17431  1stcclb  17460  2ndcdisj  17472  llyi  17490  nllyi  17491  ptpjpre1  17556  ptpjcn  17596  ptpjopn  17597  ptclsg  17600  dfac14  17603  txdis1cn  17620  pthaus  17623  hauseqlcld  17631  txkgen  17637  xkococn  17645  txcon  17674  hmeocnvcn  17746  fbssfi  17822  filss  17838  ufilss  17890  uffixfr  17908  flimneiss  17951  flimelbas  17953  fclscf  18010  flimfnfcls  18013  alexsublem  18028  alexsubb  18030  alexsubALT  18035  ptcmplem2  18037  ptcmplem3  18038  ptcmplem4  18039  tmdgsum2  18079  ghmcnp  18097  tgpt0  18101  divstgplem  18103  tsmsfbas  18110  tsmslem1  18111  tsmsgsum  18121  tsmssubm  18125  tsmsres  18126  tsmsf1o  18127  tsmsmhm  18128  tsmsadd  18129  tsmsxplem1  18135  tsmsxplem2  18136  tsmsxp  18137  istdrg2  18160  vscacn  18168  tvctdrg  18175  uspreg  18257  ucncn  18268  neipcfilu  18279  cuspcvg  18284  psmetxrge0  18297  isxmet2d  18310  prdsxmetlem  18351  imasdsf1olem  18356  xmstopn  18434  mstopn  18435  stdbdxmet  18498  prdsxmslem2  18512  nrgabv  18650  nmvs  18665  nvclvec  18685  nmoge0  18708  nghmcl  18714  nmoi  18715  nghmghm  18721  nmhmlmhm  18736  nmhmnghm  18737  icccmp  18809  xrge0gsumle  18817  xrge0tsms  18818  metds0  18833  metdstri  18834  metdsre  18836  metdseq0  18837  metdscnlem  18838  metnrmlem1a  18841  icopnfcnv  18920  xrhmeo  18924  pcoval1  18991  cphreccllem  19094  cmetcvg  19191  lmle  19207  cmscmet  19252  cmetcusp1OLD  19258  cmetcusp1  19259  hlcph  19271  minveclem4  19286  ivthlem3  19303  ovolmge0  19326  ovolicc1  19365  ovolicc2lem3  19368  ovolicc2lem5  19370  mblsplit  19381  dyadmbl  19445  mbfdm  19473  mbfadd  19506  mbfsub  19507  i1ff  19521  i1frn  19522  i1fima2  19524  mbfmul  19571  itg2monolem1  19595  bddmulibl  19683  dvnres  19770  c1liplem1  19833  c1lip2  19835  dvge0  19843  lhop1lem  19850  itgsubstlem  19885  fta1glem1  20041  fta1glem2  20042  fta1b  20045  plyf  20070  plypf1  20084  plyadd  20089  plymul  20090  coeeu  20097  dgrlem  20101  coeid  20110  elqaalem3  20191  aareccl  20196  eff1olem  20403  relogf1o  20417  logdmn0  20484  logcnlem2  20487  logcnlem3  20488  dvloglem  20492  efopnlem1  20500  efopnlem2  20501  logtayl2  20506  cxpcn3lem  20584  cxpcn3  20585  atandmneg  20699  atandmcj  20702  efiatan2  20710  cosatan  20714  cosatanne0  20715  dvatan  20728  areage0  20755  cxp2lim  20768  jensenlem2  20779  jensen  20780  wilthlem1  20804  wilth  20807  ftalem3  20810  efnnfsumcl  20838  isppw  20850  efchtdvds  20895  sqff1o  20918  dvdsdivcl  20919  fsumdvdsdiaglem  20921  dvdsppwf1o  20924  dvdsflf1o  20925  musum  20929  muinv  20931  dvdsmulf1o  20932  fsumvma2  20951  vmasum  20953  chpval2  20955  chpchtsum  20956  chpub  20957  mersenne  20964  perfect1  20965  bposlem1  21021  bposlem5  21025  bposlem6  21026  lgsfle1  21042  lgsle1  21048  lgsdirprm  21066  lgsne0  21070  lgsqrlem4  21081  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  2sqblem  21114  chebbnd1lem1  21116  chebbnd1  21119  chtppilim  21122  chpchtlim  21126  chpo1ub  21127  rplogsumlem2  21132  rpvmasumlem  21134  dchrmusumlema  21140  dchrvmasumlem1  21142  dchrisum0flblem2  21156  dchrisum0lema  21161  dchrisum0lem2a  21164  logsqvma  21189  selberg3lem2  21205  pntrsumo1  21212  pnt2  21260  ostthlem1  21274  padicabvf  21278  ostth3  21285  umgrale  21309  usgraedg2  21348  eupatrl  21643  gxneg  21807  gxadd  21816  gxmul  21819  ablocom  21826  subgoablo  21852  smgrpisass  21874  mndoisexid  21881  zrdivrng  21973  phpar2  22277  cbncms  22320  hlph  22344  hcaucvg  22641  hlimconvi  22646  shaddcl  22672  shmulcl  22673  shmulclOLD  22674  chlimi  22690  chcompl  22698  choc1  22782  nmopre  23326  cnopc  23369  lnopl  23370  unop  23371  hmop  23378  cnfnc  23386  lnfnl  23387  nlelshi  23516  cnlnadjlem5  23527  elpjidm  23640  mdslle1i  23773  mdslle2i  23774  atcv0  23798  chpssati  23819  fovcld  24003  ofrn  24005  ssnnssfz  24101  resspos  24140  resstos  24141  tleile  24142  xrge0tsmsd  24176  ofldaddlt  24194  ofld0le1  24195  subofld  24198  kerf1hrm  24215  tpr2rico  24263  rge0scvg  24288  zrhunitpreima  24315  qqhrhm  24326  esummono  24403  gsumesum  24404  esumpinfval  24416  esumpcvgval  24421  esumpmono  24422  0elsiga  24450  sigaclcu  24453  issgon  24459  sxuni  24500  isrnmeas  24507  measvuni  24521  measssd  24522  imambfm  24565  elmbfmvol2  24570  dya2icoseg2  24581  probtot  24623  ballotlem4  24709  ballotlem5  24710  ballotlemfrc  24737  ballotlemirc  24742  ballotth  24748  eldmgm  24759  dmgmaddn0  24760  dmlogdmgm  24761  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem5  24770  lgambdd  24774  lgamucov  24775  subfacp1lem3  24821  subfacp1lem5  24823  pconcn  24864  sconpht  24869  conpcon  24875  cvmcov  24903  cvmliftlem1  24925  cvmliftlem10  24934  cvmlift2lem11  24953  cvmlift2lem12  24954  fprodf1o  25225  fundmpss  25336  tfisg  25418  wfisg  25423  frinsg  25459  wfrlem5  25474  frrlem5  25499  sltval2  25524  txpss3v  25632  pprodss4v  25638  axcontlem7  25813  axcontlem10  25816  onint1  26103  mblfinlem  26143  itg2gt0cn  26159  fnetg  26244  refssfne  26264  neibastop1  26278  filnetlem3  26299  cover2  26305  indexa  26325  istotbnd3  26370  sstotbnd2  26373  sstotbnd  26374  totbndss  26376  equivtotbnd  26377  isbnd3  26383  totbndbnd  26388  equivbnd  26389  prdsbnd  26392  prdstotbnd  26393  heibor  26420  crngocom  26501  isfld2  26505  dmncrng  26556  prter2  26620  nacsfg  26649  nacsfix  26656  mzpindd  26693  diophrw  26707  diophrex  26724  rexzrexnn0  26754  pell1234qrdich  26814  rmspecnonsq  26860  rmspecfund  26862  rmspecpos  26869  monotoddzzfi  26895  ltrmxnn0  26904  rmxnn  26906  jm2.23  26957  jm3.1lem2  26979  dnnumch3  27012  lnmlssfg  27046  lnmlmic  27054  frlmsslsp  27116  frlmlbs  27117  f1lindf  27160  lnrlnm  27185  lnr2i  27188  lpirlnr  27189  hbtlem6  27201  hbt  27202  mnccoe  27211  psgnunilem5  27285  cntzsdrg  27378  idomrootle  27379  proot1mul  27383  phisum  27386  proot1hash  27387  deg1mhm  27394  stoweidlem7  27623  stoweidlem14  27630  stoweidlem16  27632  stoweidlem24  27640  stoweidlem31  27647  stoweidlem39  27655  stoweidlem50  27666  stoweidlem54  27670  stoweidlem57  27673  wallispilem3  27683  2reu1  27831  nfunsnafv  27873  faovcl  27931  usgra2pth  28041  ordelordALT  28333  2uasbanh  28359  ordelordALTVD  28688  bnj642  28822  bnj643  28823  bnj645  28824  bnj707  28829  bnj1379  28908  bnj1538  28932  bnj110  28935  bnj93  28940  bnj906  29007  bnj1006  29036  bnj1110  29057  bnj1121  29060  bnj1172  29076  bnj1204  29087  bnj1321  29102  bnj1364  29103  bnj1398  29109  bnj1450  29125  bnj1312  29133  bnj1501  29142  bnj1523  29146  toycom  29455  lsateln0  29478  lpssat  29496  lssat  29499  oposlem  29666  olop  29697  omllaw  29726  cvlexch1  29811  dihpN  31819  mapdordlem2  32120
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