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  1662  eumo  2320  2eu1  2360  reurmo  2915  pssne  3435  pssn2lp  3440  ssnpss  3442  eldifn  3462  rabsnt  3873  eldifsni  3920  unimax  4041  ssintub  4060  moop2  4443  pwssun  4481  weso  4565  ordwe  4586  reusv6OLD  4725  onminesb  4769  onminsb  4770  tfis  4825  limomss  4841  nnlim  4849  ssnlim  4854  opelxp2  4903  funmo  5461  funopg  5476  funun  5486  fununi  5508  funimaexg  5521  fndm  5535  frn  5588  f1ss  5635  f1ssr  5636  f1ssres  5637  forn  5647  f1f1orn  5676  f1orescnv  5681  f1imacnv  5682  funcocnv2  5691  dffv2  5787  exfo  5878  foelrn  5879  isorel  6037  isoini2  6050  fovcl  6166  f1opw  6290  curry1  6429  curry2  6432  f1o2ndf1  6445  fnwelem  6452  mpt2xopn0yelv  6455  f1ofveu  6575  tz7.48lem  6689  dif20el  6740  oeordi  6821  oeeulem  6835  oeeui  6836  nnawordex  6871  swoer  6924  erdisj  6943  eceqoveq  7000  mapsnconst  7050  ixpn0  7085  resixpfo  7091  boxcutc  7096  sdomnen  7127  en0  7161  en1  7165  domunsncan  7199  fodomr  7249  phplem4  7280  php3  7284  unxpdomlem3  7306  fineqvlem  7314  suppfif1  7391  f1opwfi  7401  supub  7453  suplub  7454  ordtypelem2  7477  ordtypelem3  7478  ordtypelem6  7481  ordtypelem7  7482  wemapso2  7510  wdom2d  7537  brwdom3  7539  ixpiunwdom  7548  inf3lem2  7573  inf3lem6  7577  oancom  7595  infdifsn  7600  cantnfp1lem3  7625  cantnflem3  7636  cantnflem4  7637  cantnf  7638  mapfien  7642  oef1o  7644  cnfcomlem  7645  cnfcom3  7650  tctr  7668  tz9.12lem3  7704  scottex  7798  cardid2  7829  infxpenlem  7884  acni3  7917  cardaleph  7959  iscard3  7963  dfac5lem4  7996  dfac5lem5  7997  kmlem1  8019  cofsmo  8138  fin4en1  8178  enfin2i  8190  fin23lem28  8209  fin23lem38  8218  isf32lem6  8227  enfin1ai  8253  isfin1-3  8255  hsmexlem2  8296  hsmexlem4  8298  domtriomlem  8311  axdc2lem  8317  axdc3lem2  8320  ac6num  8348  zorn2lem2  8366  brdom3  8395  alephval2  8436  alephreg  8446  pwcfsdom  8447  smobeth  8450  fpwwe2lem6  8499  fpwwe2lem13  8506  canthp1lem2  8517  pwfseqlem3  8524  hargch  8541  winalim2  8560  gchina  8563  inar1  8639  0npi  8748  mulclpi  8759  mulcanpi  8766  nlt1pi  8772  nqereu  8795  prcdnq  8859  prnmax  8861  ltresr2  9005  axrnegex  9026  axpre-sup  9033  1nuz2  10540  zsupss  10554  rpgt0  10612  ixxss1  10923  ixxss2  10924  ixxss12  10925  lbioo  10936  ubioo  10937  iccss2  10970  iccssico2  10973  elfzuz3  11045  uzdisj  11107  serge0  11365  expge0  11404  expge1  11405  expaddzlem  11411  hashfun  11688  shftfn  11876  sqrlem6  12041  rlimss  12284  lo1dm  12301  o1dm  12312  rlimrege0  12361  fsumf1o  12505  fsumge0  12562  incexc2  12606  supcvg  12623  divalglem9  12909  bitsfzolem  12934  bitsinv2  12943  bitsf1ocnv  12944  bitsf1  12946  gcdcllem1  12999  bezout  13030  prmind2  13078  nprm  13081  sqnprm  13086  dvdsprm  13087  coprm  13088  isprm5  13100  prmexpb  13105  phibndlem  13147  dfphi2  13151  phimullem  13156  pclem  13200  pcpre1  13204  pcidlem  13233  pcmpt  13249  expnprm  13259  prmreclem1  13272  prmreclem2  13273  prmreclem5  13276  1arith  13283  4sqlem18  13318  vdwnnlem3  13353  ramtlecl  13356  rami  13371  0ram  13376  ramub1lem1  13382  firest  13648  acsfiel  13867  isacs1i  13870  catlid  13896  catrid  13897  fullfo  14097  fthf1  14102  fthoppc  14108  invfuc  14159  prslem  14376  posi  14395  latlem  14465  clatlem  14527  dlatmjdi  14608  pslem  14626  tsrlin  14639  cnvtsr  14642  tsrdir  14671  mndid  14685  mhmf  14731  mhmlin  14733  mhm0  14734  grpinvex  14808  grplinv  14839  mulgz  14899  mulgdirlem  14902  mulgdir  14903  mulgass  14908  nsgbi  14959  nmzbi  14968  ghmf  14998  ghmlin  14999  conjnsg  15029  gimf1o  15038  gagrpid  15059  gaf  15060  gaass  15062  odid  15164  odf1o2  15195  gexid  15203  sylow1lem4  15223  odcau  15226  pj1id  15319  efgredeu  15372  ablcmn  15406  cmncom  15416  mulgdi  15437  gexexlem  15455  torsubg  15457  cyggenod2  15483  cygctb  15489  ghmcyg  15493  dprdf1o  15578  dprd2dlem1  15587  dprd2da  15588  ablfacrplem  15611  ablfaclem2  15632  ablfac2  15635  crngmgp  15660  rhmmhm  15813  rhmghm  15814  drngunit  15828  drngmgp  15835  drngid  15837  subrgss  15857  subrg1cl  15864  issubdrg  15881  abvge0  15901  srngcnv  15929  lmhmlin  16099  lmimf1o  16123  lvecdrng  16165  lspsolvlem  16202  islbs3  16215  lbsextlem3  16220  2idlcpbl  16293  nzrnz  16319  opprnzr  16323  rrgeq0i  16337  domneq0  16345  domnrrg  16348  drngdomn  16351  fldidom  16353  assalem  16364  mplsubrglem  16490  mplcoe1  16516  mplbas2  16519  opsrtoslem2  16533  mplelsfi  16539  coe1mul2  16650  zrngunit  16753  prmirredlem  16761  znidomb  16830  cygzn  16839  pjf  16928  toponuni  16980  tpsuni  16991  clsval2  17102  mretopd  17144  neips  17165  neiptoptop  17183  neiptopnei  17184  perflp  17206  perfi  17207  restfpw  17231  cnf  17298  cnpf  17299  cnpimaex  17308  cnima  17317  t0sep  17376  t1sncld  17378  t1ficld  17379  hausnei  17380  regsep  17386  pnrmcld  17394  nrmsep3  17407  cnrmi  17412  cmpcov  17440  discmp  17449  tgcmp  17452  uncmp  17454  hauscmplem  17457  cmpfi  17459  conclo  17466  1stcclb  17495  2ndcdisj  17507  llyi  17525  nllyi  17526  ptpjpre1  17591  ptpjcn  17631  ptpjopn  17632  ptclsg  17635  dfac14  17638  txdis1cn  17655  pthaus  17658  hauseqlcld  17666  txkgen  17672  xkococn  17680  txcon  17709  hmeocnvcn  17781  fbssfi  17857  filss  17873  ufilss  17925  uffixfr  17943  flimneiss  17986  flimelbas  17988  fclscf  18045  flimfnfcls  18048  alexsublem  18063  alexsubb  18065  alexsubALT  18070  ptcmplem2  18072  ptcmplem3  18073  ptcmplem4  18074  tmdgsum2  18114  ghmcnp  18132  tgpt0  18136  divstgplem  18138  tsmsfbas  18145  tsmslem1  18146  tsmsgsum  18156  tsmssubm  18160  tsmsres  18161  tsmsf1o  18162  tsmsmhm  18163  tsmsadd  18164  tsmsxplem1  18170  tsmsxplem2  18171  tsmsxp  18172  istdrg2  18195  vscacn  18203  tvctdrg  18210  uspreg  18292  ucncn  18303  neipcfilu  18314  cuspcvg  18319  psmetxrge0  18332  isxmet2d  18345  prdsxmetlem  18386  imasdsf1olem  18391  xmstopn  18469  mstopn  18470  stdbdxmet  18533  prdsxmslem2  18547  nrgabv  18685  nmvs  18700  nvclvec  18720  nmoge0  18743  nghmcl  18749  nmoi  18750  nghmghm  18756  nmhmlmhm  18771  nmhmnghm  18772  icccmp  18844  xrge0gsumle  18852  xrge0tsms  18853  metds0  18868  metdstri  18869  metdsre  18871  metdseq0  18872  metdscnlem  18873  metnrmlem1a  18876  icopnfcnv  18955  xrhmeo  18959  pcoval1  19026  cphreccllem  19129  cmetcvg  19226  lmle  19242  cmscmet  19287  cmetcusp1OLD  19293  cmetcusp1  19294  hlcph  19306  minveclem4  19321  ivthlem3  19338  ovolmge0  19361  ovolicc1  19400  ovolicc2lem3  19403  ovolicc2lem5  19405  mblsplit  19416  dyadmbl  19480  mbfdm  19508  mbfadd  19541  mbfsub  19542  i1ff  19556  i1frn  19557  i1fima2  19559  mbfmul  19606  itg2monolem1  19630  bddmulibl  19718  dvnres  19805  c1liplem1  19868  c1lip2  19870  dvge0  19878  lhop1lem  19885  itgsubstlem  19920  fta1glem1  20076  fta1glem2  20077  fta1b  20080  plyf  20105  plypf1  20119  plyadd  20124  plymul  20125  coeeu  20132  dgrlem  20136  coeid  20145  elqaalem3  20226  aareccl  20231  eff1olem  20438  relogf1o  20452  logdmn0  20519  logcnlem2  20522  logcnlem3  20523  dvloglem  20527  efopnlem1  20535  efopnlem2  20536  logtayl2  20541  cxpcn3lem  20619  cxpcn3  20620  atandmneg  20734  atandmcj  20737  efiatan2  20745  cosatan  20749  cosatanne0  20750  dvatan  20763  areage0  20790  cxp2lim  20803  jensenlem2  20814  jensen  20815  wilthlem1  20839  wilth  20842  ftalem3  20845  efnnfsumcl  20873  isppw  20885  efchtdvds  20930  sqff1o  20953  dvdsdivcl  20954  fsumdvdsdiaglem  20956  dvdsppwf1o  20959  dvdsflf1o  20960  musum  20964  muinv  20966  dvdsmulf1o  20967  fsumvma2  20986  vmasum  20988  chpval2  20990  chpchtsum  20991  chpub  20992  mersenne  20999  perfect1  21000  bposlem1  21056  bposlem5  21060  bposlem6  21061  lgsfle1  21077  lgsle1  21083  lgsdirprm  21101  lgsne0  21105  lgsqrlem4  21116  lgseisenlem3  21123  lgseisenlem4  21124  lgsquadlem1  21126  lgsquadlem2  21127  2sqblem  21149  chebbnd1lem1  21151  chebbnd1  21154  chtppilim  21157  chpchtlim  21161  chpo1ub  21162  rplogsumlem2  21167  rpvmasumlem  21169  dchrmusumlema  21175  dchrvmasumlem1  21177  dchrisum0flblem2  21191  dchrisum0lema  21196  dchrisum0lem2a  21199  logsqvma  21224  selberg3lem2  21240  pntrsumo1  21247  pnt2  21295  ostthlem1  21309  padicabvf  21313  ostth3  21320  umgrale  21344  usgraedg2  21383  eupatrl  21678  gxneg  21842  gxadd  21851  gxmul  21854  ablocom  21861  subgoablo  21887  smgrpisass  21909  mndoisexid  21916  zrdivrng  22008  phpar2  22312  cbncms  22355  hlph  22379  hcaucvg  22676  hlimconvi  22681  shaddcl  22707  shmulcl  22708  shmulclOLD  22709  chlimi  22725  chcompl  22733  choc1  22817  nmopre  23361  cnopc  23404  lnopl  23405  unop  23406  hmop  23413  cnfnc  23421  lnfnl  23422  nlelshi  23551  cnlnadjlem5  23562  elpjidm  23675  mdslle1i  23808  mdslle2i  23809  atcv0  23833  chpssati  23854  fovcld  24038  ofrn  24040  ssnnssfz  24136  resspos  24175  resstos  24176  tleile  24177  xrge0tsmsd  24211  ofldaddlt  24229  ofld0le1  24230  subofld  24233  kerf1hrm  24250  tpr2rico  24298  rge0scvg  24323  zrhunitpreima  24350  qqhrhm  24361  esummono  24438  gsumesum  24439  esumpinfval  24451  esumpcvgval  24456  esumpmono  24457  0elsiga  24485  sigaclcu  24488  issgon  24494  sxuni  24535  isrnmeas  24542  measvuni  24556  measssd  24557  imambfm  24600  elmbfmvol2  24605  dya2icoseg2  24616  probtot  24658  ballotlem4  24744  ballotlem5  24745  ballotlemfrc  24772  ballotlemirc  24777  ballotth  24783  eldmgm  24794  dmgmaddn0  24795  dmlogdmgm  24796  lgamgulmlem2  24802  lgamgulmlem3  24803  lgamgulmlem5  24805  lgambdd  24809  lgamucov  24810  subfacp1lem3  24856  subfacp1lem5  24858  pconcn  24899  sconpht  24904  conpcon  24910  cvmcov  24938  cvmliftlem1  24960  cvmliftlem10  24969  cvmlift2lem11  24988  cvmlift2lem12  24989  fprodf1o  25261  fundmpss  25377  tfisg  25459  wfisg  25464  frinsg  25500  wfrlem5  25515  frrlem5  25540  sltval2  25565  txpss3v  25673  pprodss4v  25679  axcontlem7  25857  axcontlem10  25860  onint1  26147  mblfinlem  26190  itg2gt0cn  26206  fnetg  26291  refssfne  26311  neibastop1  26325  filnetlem3  26346  cover2  26352  indexa  26372  istotbnd3  26417  sstotbnd2  26420  sstotbnd  26421  totbndss  26423  equivtotbnd  26424  isbnd3  26430  totbndbnd  26435  equivbnd  26436  prdsbnd  26439  prdstotbnd  26440  heibor  26467  crngocom  26548  isfld2  26552  dmncrng  26603  prter2  26667  nacsfg  26696  nacsfix  26703  mzpindd  26740  diophrw  26754  diophrex  26771  rexzrexnn0  26801  pell1234qrdich  26861  rmspecnonsq  26907  rmspecfund  26909  rmspecpos  26916  monotoddzzfi  26942  ltrmxnn0  26951  rmxnn  26953  jm2.23  27004  jm3.1lem2  27026  dnnumch3  27059  lnmlssfg  27093  lnmlmic  27101  frlmsslsp  27163  frlmlbs  27164  f1lindf  27207  lnrlnm  27232  lnr2i  27235  lpirlnr  27236  hbtlem6  27248  hbt  27249  mnccoe  27258  psgnunilem5  27332  cntzsdrg  27425  idomrootle  27426  proot1mul  27430  phisum  27433  proot1hash  27434  deg1mhm  27441  stoweidlem7  27670  stoweidlem14  27677  stoweidlem16  27679  stoweidlem24  27687  stoweidlem31  27694  stoweidlem39  27702  stoweidlem50  27713  stoweidlem54  27717  stoweidlem57  27720  wallispilem3  27730  2reu1  27878  nfunsnafv  27920  faovcl  27978  usgra2pth  28185  ordelordALT  28477  2uasbanh  28503  ordelordALTVD  28833  bnj642  28970  bnj643  28971  bnj645  28972  bnj707  28977  bnj1379  29056  bnj1538  29080  bnj110  29083  bnj93  29088  bnj906  29155  bnj1006  29184  bnj1110  29205  bnj1121  29208  bnj1172  29224  bnj1204  29235  bnj1321  29250  bnj1364  29251  bnj1398  29257  bnj1450  29273  bnj1312  29281  bnj1501  29290  bnj1523  29294  toycom  29609  lsateln0  29632  lpssat  29650  lssat  29653  oposlem  29820  olop  29851  omllaw  29880  cvlexch1  29965  dihpN  31973  mapdordlem2  32274
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