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

Theorem simprbi 464
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 194 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 463 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  xornan  1371  sb1  1743  eumo  2314  2eu1OLD  2377  reurmo  3075  pssne  3596  pssn2lp  3601  ssnpss  3603  eldifn  3623  rabsnt  4109  eldifsni  4158  unimax  4287  ssintub  4306  reusv6OLD  4667  moop2  4751  pwssun  4795  weso  4879  ordwe  4900  opelxp2  5042  eldmeldmressn  5324  funmo  5610  funopg  5626  funun  5636  fununi  5660  funimaexg  5671  fndm  5686  frn  5743  f1ss  5792  f1ssr  5793  f1ssres  5794  forn  5804  f1f1orn  5833  f1orescnv  5837  f1imacnv  5838  funcocnv2  5846  dffv2  5946  exfo  6050  foelrn  6051  isorel  6223  isoini2  6236  f1ofveu  6291  fovcl  6406  f1opw  6528  onminesb  6632  onminsb  6633  tfis  6688  limomss  6704  nnlim  6712  ssnlim  6717  curry1  6891  curry2  6894  f1o2ndf1  6907  fnwelem  6914  ressuppss  6937  mpt2xopn0yelv  6959  tz7.48lem  7124  dif20el  7173  oeordi  7254  oeeulem  7268  oeeui  7269  nnawordex  7304  swoer  7357  erdisj  7377  eceqoveq  7434  mapsnconst  7483  ixpn0  7520  resixpfo  7526  boxcutc  7531  sdomnen  7563  en0  7597  en1  7601  domunsncan  7636  fodomr  7687  phplem4  7718  php3  7722  unxpdomlem3  7745  fineqvlem  7753  f1opwfi  7842  fsuppcolem  7878  fsuppco  7879  mapfienlem1  7882  mapfienlem2  7883  supub  7936  suplub  7937  ordtypelem2  7962  ordtypelem3  7963  ordtypelem6  7966  ordtypelem7  7967  wemapso2OLD  7995  wemapso2lem  7996  wdom2d  8024  brwdom3  8026  ixpiunwdom  8035  inf3lem2  8063  inf3lem6  8067  oancom  8085  infdifsn  8090  cantnfp1lem3  8116  cantnflem3  8127  cantnflem4  8128  cantnfp1lem3OLD  8142  cantnflem3OLD  8149  cantnflem4OLD  8150  cantnfOLD  8151  mapfienOLD  8155  oef1o  8158  oef1oOLD  8159  cnfcom3  8165  cnfcomlemOLD  8168  cnfcom3OLD  8173  tctr  8188  tz9.12lem3  8224  scottex  8320  cardid2  8351  infxpenlem  8408  acni3  8445  cardaleph  8487  iscard3  8491  dfac5lem4  8524  dfac5lem5  8525  kmlem1  8547  cofsmo  8666  fin4en1  8706  enfin2i  8718  fin23lem28  8737  fin23lem38  8746  isf32lem6  8755  enfin1ai  8781  isfin1-3  8783  hsmexlem2  8824  hsmexlem4  8826  domtriomlem  8839  axdc2lem  8845  axdc3lem2  8848  ac6num  8876  zorn2lem2  8894  brdom3  8923  alephval2  8964  alephreg  8974  pwcfsdom  8975  smobeth  8978  fpwwe2lem6  9030  fpwwe2lem13  9037  canthp1lem2  9048  pwfseqlem3  9055  hargch  9068  winalim2  9091  gchina  9094  inar1  9170  0npi  9277  mulclpi  9288  mulcanpi  9295  nlt1pi  9301  nqereu  9324  prcdnq  9388  prnmax  9390  ltresr2  9535  axrnegex  9556  axpre-sup  9563  1nuz2  11182  zsupss  11196  rpgt0  11256  ixxss1  11572  ixxss2  11573  ixxss12  11574  lbioo  11585  ubioo  11586  iccss2  11620  iccssico2  11623  elfzuz3  11710  uzdisj  11776  nn0disj  11816  serge0  12163  expge0  12204  expge1  12205  expaddzlem  12211  hashrabsn1  12444  hashfun  12498  shftfn  12917  sqrlem6  13092  rlimss  13336  lo1dm  13353  o1dm  13364  rlimrege0  13413  fsumf1o  13556  fsumge0  13620  incexc2  13661  supcvg  13678  fprodf1o  13764  divalglem9  14070  bitsfzolem  14095  bitsinv2  14104  bitsf1ocnv  14105  bitsf1  14107  gcdcllem1  14160  bezout  14191  prmind2  14239  nprm  14242  sqnprm  14250  dvdsprm  14251  coprm  14252  isprm5  14264  phibndlem  14311  dfphi2  14315  phimullem  14320  pclem  14373  pcpre1  14377  pcidlem  14406  expnprm  14432  prmreclem1  14445  prmreclem2  14446  prmreclem5  14449  1arith  14456  4sqlem18  14491  vdwnnlem3  14526  ramtlecl  14529  rami  14544  0ram  14549  ramub1lem1  14555  firest  14849  acsfiel  15070  isacs1i  15073  catlid  15099  catrid  15100  fullfo  15327  fthf1  15332  fthoppc  15338  invfuc  15389  prslem  15686  posi  15705  dlatmjdi  15950  pslem  15962  tsrlin  15975  cnvtsr  15978  tsrdir  15994  mndid  16059  mhmf  16097  mhmlin  16099  mhm0  16100  mrcmndind  16123  grpinvex  16191  grplinv  16222  mulgz  16289  mulgdirlem  16292  mulgdir  16293  mulgass  16298  nsgbi  16358  nmzbi  16367  ghmf  16397  ghmlin  16398  conjnsg  16428  gimf1o  16437  gagrpid  16458  gaf  16459  gaass  16461  psgnunilem5  16645  odid  16688  odf1o2  16719  gexid  16727  sylow1lem4  16747  odcau  16750  pj1id  16843  efgredeu  16896  ablcmn  16930  cmncom  16940  mulgdi  16961  gexexlem  16984  torsubg  16986  cyggenod2  17014  cygctb  17020  ghmcyg  17024  dprdf1o  17205  dprd2dlem1  17216  dprd2da  17217  ablfacrplem  17242  ablfaclem2  17263  ablfac2  17266  crngmgp  17332  rhmmhm  17497  rhmghm  17500  drngunit  17527  drngmgp  17534  drngid  17536  subrgss  17556  subrg1cl  17563  issubdrg  17580  abvge0  17600  srngcnv  17628  lmhmlin  17807  lmimf1o  17835  lvecdrng  17877  lspsolvlem  17914  islbs3  17927  lbsextlem3  17932  2idlcpbl  18008  nzrnz  18034  opprnzr  18039  rrgeq0i  18063  domneq0  18072  domnrrg  18075  drngdomn  18078  fldidom  18080  assalem  18091  mplsubrglem  18226  mplsubrglemOLD  18227  mplcoe1  18253  mplbas2  18260  mplbas2OLD  18261  opsrtoslem2  18275  mplelsfi  18281  mplelsfiOLD  18282  coe1mul2  18436  zringunit  18646  zrngunit  18647  prmirredlem  18649  prmirredlemOLD  18652  znidomb  18726  cygzn  18735  psgndiflemB  18762  pjf  18870  frlmsslsp  18955  frlmsslspOLD  18956  frlmlbs  18957  f1lindf  18983  pmatcoe1fsupp  19328  toponuni  19554  tpsuni  19565  clsval2  19677  mretopd  19719  neips  19740  neiptoptop  19758  neiptopnei  19759  perflp  19781  perfi  19782  restfpw  19806  cnf  19873  cnpf  19874  cnpimaex  19883  cnima  19892  t0sep  19951  t1sncld  19953  t1ficld  19954  hausnei  19955  regsep  19961  pnrmcld  19969  nrmsep3  19982  cnrmi  19987  cmpcov  20015  discmp  20024  tgcmp  20027  uncmp  20029  hauscmplem  20032  cmpfi  20034  conclo  20041  1stcclb  20070  2ndcdisj  20082  llyi  20100  nllyi  20101  ptpjpre1  20197  ptpjcn  20237  ptpjopn  20238  ptclsg  20241  dfac14  20244  txdis1cn  20261  pthaus  20264  hauseqlcld  20272  txkgen  20278  xkococn  20286  txcon  20315  hmeocnvcn  20387  fbssfi  20463  filss  20479  ufilss  20531  uffixfr  20549  flimneiss  20592  flimelbas  20594  fclscf  20651  flimfnfcls  20654  alexsublem  20669  alexsubb  20671  alexsubALT  20676  ptcmplem2  20678  ptcmplem3  20679  ptcmplem4  20680  tmdgsum2  20720  ghmcnp  20738  tgpt0  20742  qustgplem  20744  tsmsfbas  20751  tsmslem1  20752  tsmsgsum  20762  tsmsgsumOLD  20765  tsmssubm  20769  tsmsresOLD  20770  tsmsres  20771  tsmsf1o  20772  tsmsmhm  20773  tsmsadd  20774  tsmsxplem1  20780  tsmsxplem2  20781  tsmsxp  20782  istdrg2  20805  vscacn  20813  tvctdrg  20820  uspreg  20902  ucncn  20913  neipcfilu  20924  cuspcvg  20929  psmetxrge0  20942  isxmet2d  20955  prdsxmetlem  20996  imasdsf1olem  21001  xmstopn  21079  mstopn  21080  stdbdxmet  21143  prdsxmslem2  21157  nrgabv  21295  nmvs  21310  nvclvec  21330  nmoge0  21353  nghmcl  21359  nmoi  21360  nghmghm  21366  nmhmlmhm  21381  nmhmnghm  21382  icccmp  21455  xrge0gsumle  21463  xrge0tsms  21464  metds0  21479  metdstri  21480  metdsre  21482  metdseq0  21483  metdscnlem  21484  metnrmlem1a  21487  icopnfcnv  21567  xrhmeo  21571  pcoval1  21638  cvslvec  21731  cvsunit  21733  cphreccllem  21750  cmetcvg  21849  lmle  21865  cmscmet  21910  cmetcusp1OLD  21916  cmetcusp1  21917  hlcph  21929  minveclem4  21972  ivthlem3  21990  ovolmge0  22013  ovolicc1  22052  ovolicc2lem3  22055  ovolicc2lem5  22057  mblsplit  22068  dyadmbl  22134  mbfdm  22160  mbfadd  22193  mbfsub  22194  i1ff  22208  i1frn  22209  i1fima2  22211  mbfmul  22258  itg2monolem1  22282  bddmulibl  22370  dvnres  22459  c1liplem1  22522  c1lip2  22524  dvge0  22532  lhop1lem  22539  itgsubstlem  22574  fta1glem1  22691  fta1glem2  22692  fta1b  22695  plyf  22720  plypf1  22734  plyadd  22739  plymul  22740  coeeu  22747  dgrlem  22751  coeid  22760  elqaalem3  22842  aareccl  22847  eff1olem  23060  relogf1o  23079  logdmn0  23146  logcnlem2  23149  logcnlem3  23150  dvloglem  23154  efopnlem1  23162  efopnlem2  23163  logtayl2  23168  cxpcn3lem  23246  cxpcn3  23247  atandmneg  23362  atandmcj  23365  efiatan2  23373  cosatan  23377  cosatanne0  23378  dvatan  23391  areage0  23418  cxp2lim  23431  jensenlem2  23442  jensen  23443  wilthlem1  23467  wilth  23470  ftalem3  23473  efnnfsumcl  23501  isppw  23513  efchtdvds  23558  sqff1o  23581  dvdsdivcl  23582  fsumdvdsdiaglem  23584  dvdsppwf1o  23587  dvdsflf1o  23588  musum  23592  muinv  23594  dvdsmulf1o  23595  fsumvma2  23614  vmasum  23616  chpval2  23618  chpchtsum  23619  chpub  23620  mersenne  23627  perfect1  23628  bposlem1  23684  bposlem5  23688  lgsfle1  23705  lgsle1  23711  lgsdirprm  23729  lgsne0  23733  lgsqrlem4  23744  lgseisenlem3  23751  lgseisenlem4  23752  lgsquadlem1  23754  lgsquadlem2  23755  2sqblem  23777  chebbnd1lem1  23779  chebbnd1  23782  chtppilim  23785  chpchtlim  23789  chpo1ub  23790  rplogsumlem2  23795  rpvmasumlem  23797  dchrmusumlema  23803  dchrvmasumlem1  23805  dchrisum0flblem2  23819  dchrisum0lema  23824  dchrisum0lem2a  23827  logsqvma  23852  selberg3lem2  23868  pntrsumo1  23875  pnt2  23923  ostthlem1  23937  ostth3  23948  axtgcgrrflx  23984  axtgcgrid  23985  axtgsegcon  23986  axtg5seg  23987  axtgbtwnid  23988  axtgpasch  23989  axtgcont1  23990  tglng  24058  axcontlem7  24399  axcontlem10  24402  umgrale  24447  usgraedg2  24501  usgraexmpledg  24529  clwlkfclwwlk1hashn  24967  eupatrl  25094  gxneg  25394  gxadd  25403  gxmul  25406  ablocom  25413  subgoablo  25439  smgrpisass  25461  mndoisexid  25468  zrdivrng  25560  phpar2  25864  cbncms  25907  hlph  25931  hcaucvg  26229  hlimconvi  26234  shaddcl  26260  shmulcl  26261  shmulclOLD  26262  chlimi  26278  chcompl  26286  choc1  26371  nmopre  26915  cnopc  26958  lnopl  26959  unop  26960  hmop  26967  cnfnc  26975  lnfnl  26976  nlelshi  27105  cnlnadjlem5  27116  elpjidm  27229  mdslle1i  27362  mdslle2i  27363  atcv0  27387  chpssati  27408  elin2d  27546  fovcld  27621  aciunf1lem  27650  ssnnssfz  27749  ressprs  27795  oduprs  27796  resspos  27799  resstos  27800  tleile  27801  ogrpinvOLD  27857  ogrpinv0le  27858  ogrpsub  27859  ogrpaddlt  27860  isarchi3  27883  archirng  27884  archirngz  27885  archiabllem1a  27887  archiabllem1b  27888  archiabllem2a  27890  archiabllem2c  27891  archiabllem2b  27892  archiabl  27894  xrge0tsmsd  27928  orngsqr  27947  ornglmulle  27948  orngrmulle  27949  ofldtos  27954  ofldlt1  27956  ofldchr  27957  suborng  27958  subofld  27959  isarchiofld  27960  nn0omnd  27984  qtophaus  27992  crefi  28003  cmpcref  28006  cmppcmp  28014  pcmplfin  28016  tpr2rico  28047  rge0scvg  28084  zrhunitpreima  28112  qqhrhm  28123  esummono  28221  gsumesum  28222  esumpinfval  28235  esumpcvgval  28240  esumpmono  28241  0elsiga  28275  sigaclcu  28278  issgon  28284  sxuni  28325  isrnmeas  28332  measvuni  28346  measssd  28347  ddemeas  28369  imambfm  28394  elmbfmvol2  28399  dya2icoseg2  28410  omssubaddlem  28431  omssubadd  28432  sibfinima  28456  oddpwdc  28468  oddpwdcv  28469  eulerpartlemf  28484  eulerpartlemt  28485  eulerpartlemr  28488  eulerpartlemgvv  28490  eulerpartlemgs2  28494  sseqf  28506  fiblem  28512  probtot  28526  ballotlem4  28612  ballotlem5  28613  ballotlemfrc  28640  ballotlemirc  28645  ballotth  28651  eldmgm  28739  dmgmaddn0  28740  dmlogdmgm  28741  lgamgulmlem2  28747  lgamgulmlem3  28748  lgamgulmlem5  28750  lgambdd  28754  lgamucov  28755  subfacp1lem3  28801  subfacp1lem5  28803  pconcn  28844  sconpht  28849  conpcon  28855  cvmcov  28883  cvmliftlem1  28905  cvmliftlem10  28914  cvmlift2lem11  28933  cvmlift2lem12  28934  msubff1  29091  mvhf1  29094  mthmpps  29117  mclspps  29119  fundmpss  29371  tfisg  29458  wfisg  29463  frinsg  29499  wfrlem5  29521  frrlem5  29565  sltval2  29590  txpss3v  29690  pprodss4v  29696  onint1  30076  wl-nfeqfb  30152  fin2solem  30201  fin2so  30202  ptrest  30210  mblfinlem2  30214  dvtan  30227  itg2gt0cn  30232  ftc1anclem7  30258  ftc1anclem8  30259  ftc1anc  30260  fnetg  30325  neibastop1  30339  filnetlem3  30360  cover2  30366  indexa  30386  istotbnd3  30429  sstotbnd2  30432  sstotbnd  30433  totbndss  30435  equivtotbnd  30436  isbnd3  30442  totbndbnd  30447  equivbnd  30448  prdsbnd  30451  prdstotbnd  30452  heibor  30479  crngocom  30560  isfld2  30564  dmncrng  30615  prter2  30784  nacsfg  30799  nacsfix  30806  mzpindd  30840  diophrw  30854  diophrex  30871  rexzrexnn0  30899  pell1234qrdich  30959  rmspecsqrtnq  31004  rmspecnonsq  31005  rmspecfund  31007  rmspecpos  31014  monotoddzzfi  31040  ltrmxnn0  31049  rmxnn  31051  jm2.23  31100  jm3.1lem2  31122  dnnumch3  31155  lnmlssfg  31188  lnmlmic  31196  lnrlnm  31224  lnr2i  31227  lpirlnr  31228  hbtlem6  31240  hbt  31241  mnccoe  31249  cntzsdrg  31313  idomrootle  31314  proot1mul  31318  phisum  31321  proot1hash  31322  deg1mhm  31329  radcnvrat  31357  binomcxplemdvbinom  31420  binomcxplemcvg  31421  binomcxplemnotnn0  31423  elinel2  31584  sumnnodd  31797  stoweidlem7  31950  stoweidlem14  31957  stoweidlem16  31959  stoweidlem24  31967  stoweidlem31  31974  stoweidlem54  31997  wallispilem3  32010  fourierdlem42  32092  fourierdlem48  32098  fourierdlem51  32101  fourierdlem64  32114  fourierdlem76  32126  fourierdlem79  32129  fourierdlem81  32131  fourierdlem87  32137  etransclem28  32206  etransclem32  32210  2reu1  32352  nfunsnafv  32388  faovcl  32446  usgra2pth  32574  clintopcllaw  32755  0ringbas  32779  rnghmmgmhm  32802  uzlidlring  32837  rnghmsubcsetclem1  32885  rngccatidOLD  32899  zrinitorngc  32910  zrtermorngc  32911  rhmsubcsetclem1  32931  funcringcsetcOLD2lem7  32952  ringccatidOLD  32962  funcringcsetclem7OLD  32975  irinitoringc  32979  zrtermoringc  32980  fldhmsubc  32994  fldhmsubcOLD  33013  ssnn0ssfz  33040  el0ldepsnzr  33170  ordelordALT  33409  2uasbanh  33435  ordelordALTVD  33768  bnj642  33906  bnj643  33907  bnj645  33908  bnj707  33913  bnj1379  33990  bnj1538  34014  bnj110  34017  bnj93  34022  bnj906  34089  bnj1006  34118  bnj1110  34139  bnj1121  34142  bnj1172  34158  bnj1204  34169  bnj1321  34184  bnj1364  34185  bnj1398  34191  bnj1450  34207  bnj1312  34215  bnj1501  34224  bnj1523  34228  bj-elid2  34701  toycom  34799  lsateln0  34821  lpssat  34839  lssat  34842  oposlem  35008  olop  35040  omllaw  35069  cvlexch1  35154  dihpN  37164  mapdordlem2  37465
  Copyright terms: Public domain W3C validator