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

Theorem simprbi 450
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 186 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 449 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  sb1  1632  eumo  2183  2eu1  2223  reurmo  2755  pssne  3272  pssn2lp  3277  ssnpss  3279  eldifn  3299  rabsnt  3704  eldifsni  3750  unimax  3861  ssintub  3880  moop2  4261  pwssun  4299  weso  4384  ordwe  4405  reusv6OLD  4545  onminesb  4589  onminsb  4590  tfis  4645  limomss  4661  nnlim  4669  ssnlim  4674  opelxp2  4723  funmo  5271  funopg  5286  funun  5296  fununi  5316  funimaexg  5329  fndm  5343  frn  5395  f1ss  5442  f1ssr  5443  f1ssres  5444  forn  5454  f1f1orn  5483  f1orescnv  5488  f1imacnv  5489  funcocnv2  5498  dffv2  5592  exfo  5678  foelrn  5679  f1fveq  5786  isorel  5823  isoini2  5836  fovcl  5949  f1opw  6072  curry1  6210  curry2  6213  fnwelem  6230  f1ofveu  6339  tz7.48lem  6453  dif20el  6504  oeordi  6585  oeeulem  6599  oeeui  6600  nnawordex  6635  swoer  6688  erdisj  6707  eceqoveq  6763  mapsnconst  6813  ixpn0  6848  resixpfo  6854  boxcutc  6859  sdomnen  6890  en0  6924  en1  6928  domunsncan  6962  fodomr  7012  phplem4  7043  php3  7047  unxpdomlem3  7069  fineqvlem  7077  suppfif1  7149  f1opwfi  7159  supub  7210  suplub  7211  ordtypelem2  7234  ordtypelem3  7235  ordtypelem6  7238  ordtypelem7  7239  wemapso2  7267  wdom2d  7294  brwdom3  7296  ixpiunwdom  7305  inf3lem2  7330  inf3lem6  7334  oancom  7352  infdifsn  7357  cantnfp1lem3  7382  cantnflem3  7393  cantnflem4  7394  cantnf  7395  mapfien  7399  oef1o  7401  cnfcomlem  7402  cnfcom3  7407  tctr  7425  tz9.12lem3  7461  scottex  7555  cardid2  7586  infxpenlem  7641  acni3  7674  cardaleph  7716  iscard3  7720  dfac5lem4  7753  dfac5lem5  7754  kmlem1  7776  cofsmo  7895  fin4en1  7935  enfin2i  7947  fin23lem28  7966  fin23lem38  7975  isf32lem6  7984  enfin1ai  8010  isfin1-3  8012  hsmexlem2  8053  hsmexlem4  8055  domtriomlem  8068  axdc2lem  8074  axdc3lem2  8077  ac6num  8106  zorn2lem2  8124  brdom3  8153  alephval2  8194  alephreg  8204  pwcfsdom  8205  smobeth  8208  fpwwe2lem6  8257  fpwwe2lem13  8264  canthp1lem2  8275  pwfseqlem3  8282  hargch  8299  winalim2  8318  gchina  8321  inar1  8397  0npi  8506  mulclpi  8517  mulcanpi  8524  nlt1pi  8530  nqereu  8553  enqeq  8558  prcdnq  8617  prnmax  8619  ltresr2  8763  axrnegex  8784  axpre-sup  8791  1nuz2  10293  zsupss  10307  rpgt0  10365  ixxss1  10674  ixxss2  10675  ixxss12  10676  lbioo  10687  ubioo  10688  iccss2  10720  iccssico2  10723  elfzuz3  10795  uzdisj  10856  serge0  11100  expge0  11138  expge1  11139  expaddzlem  11145  hashfun  11389  shftfn  11568  sqrlem6  11733  eqsqrd  11851  rlimss  11976  lo1dm  11993  o1dm  12004  rlimrege0  12053  fsumf1o  12196  fsumge0  12253  incexc2  12297  supcvg  12314  divalglem9  12600  bitsfzolem  12625  bitsinv2  12634  bitsf1ocnv  12635  bitsf1  12637  gcdcllem1  12690  bezout  12721  prmind2  12769  nprm  12772  sqnprm  12777  dvdsprm  12778  coprm  12779  isprm5  12791  prmexpb  12796  phibndlem  12838  dfphi2  12842  phimullem  12847  pclem  12891  pcpre1  12895  pcidlem  12924  pcmpt  12940  expnprm  12950  prmreclem1  12963  prmreclem2  12964  prmreclem5  12967  1arith  12974  4sqlem18  13009  vdwnnlem3  13044  ramtlecl  13047  rami  13062  0ram  13067  ramub1lem1  13073  firest  13337  acsfiel  13556  isacs1i  13559  catlid  13585  catrid  13586  fullfo  13786  fthf1  13791  fthoppc  13797  invfuc  13848  prslem  14065  posi  14084  latlem  14154  clatlem  14216  dlatmjdi  14297  pslem  14315  tsrlin  14328  cnvtsr  14331  tsrdir  14360  mndid  14374  mhmf  14420  mhmlin  14422  mhm0  14423  grpinvex  14497  grplinv  14528  mulgz  14588  mulgdirlem  14591  mulgdir  14592  mulgass  14597  nsgbi  14648  nmzbi  14657  ghmf  14687  ghmlin  14688  conjnsg  14718  gimf1o  14727  gagrpid  14748  gaf  14749  gaass  14751  odid  14853  odf1o2  14884  gexid  14892  sylow1lem4  14912  odcau  14915  pj1id  15008  efgredeu  15061  efgred2  15062  ablcmn  15095  cmncom  15105  mulgdi  15126  gexexlem  15144  torsubg  15146  frgpnabllem2  15162  cyggenod2  15172  cygctb  15178  ghmcyg  15182  dprdf1o  15267  dprd2dlem1  15276  dprd2da  15277  ablfacrplem  15300  ablfaclem2  15321  ablfac2  15324  crngmgp  15349  rhmmhm  15502  rhmghm  15503  drngunit  15517  drngmgp  15524  drngid  15526  subrgss  15546  subrg1cl  15553  issubdrg  15570  abvge0  15590  srngcnv  15618  lmhmlin  15792  lmimf1o  15816  lvecdrng  15858  lspsolvlem  15895  islbs3  15908  lbsextlem3  15913  2idlcpbl  15986  nzrnz  16012  opprnzr  16016  rrgeq0i  16030  domneq0  16038  domnrrg  16041  drngdomn  16044  fldidom  16046  assalem  16057  mplsubrglem  16183  mplcoe1  16209  mplbas2  16212  opsrtoslem2  16226  mplelsfi  16232  coe1mul2  16346  zrngunit  16438  prmirredlem  16446  znidomb  16515  cygzn  16524  frgpcyg  16527  pjf  16613  toponuni  16665  tpsuni  16676  clsval2  16787  mretopd  16829  neips  16850  perflp  16885  perfi  16886  restfpw  16910  cnf  16976  cnpf  16977  cnpimaex  16986  cnima  16994  t0sep  17052  t1sncld  17054  t1ficld  17055  hausnei  17056  regsep  17062  pnrmcld  17070  nrmsep3  17083  cnrmi  17088  cmpcov  17116  discmp  17125  tgcmp  17128  uncmp  17130  hauscmplem  17133  cmpfi  17135  conclo  17141  1stcclb  17170  2ndcdisj  17182  llyi  17200  nllyi  17201  ptpjpre1  17266  ptpjcn  17305  ptpjopn  17306  ptclsg  17309  dfac14  17312  txdis1cn  17329  pthaus  17332  hauseqlcld  17340  txkgen  17346  xkococn  17354  txcon  17383  hmeocnvcn  17452  qtophmeo  17508  fbssfi  17532  filss  17548  ufilss  17600  uffixfr  17618  flimneiss  17661  flimelbas  17663  fclscf  17720  flimfnfcls  17723  alexsublem  17738  alexsubb  17740  alexsubALT  17745  ptcmplem2  17747  ptcmplem3  17748  ptcmplem4  17749  tmdgsum2  17779  ghmcnp  17797  tgpt0  17801  divstgplem  17803  tsmsfbas  17810  tsmslem1  17811  tsmsgsum  17821  tsmssubm  17825  tsmsres  17826  tsmsf1o  17827  tsmsmhm  17828  tsmsadd  17829  tsmsxplem1  17835  tsmsxplem2  17836  tsmsxp  17837  istdrg2  17860  vscacn  17868  tvctdrg  17875  isxmet2d  17892  prdsxmetlem  17932  imasdsf1olem  17937  xmstopn  17997  mstopn  17998  stdbdxmet  18061  prdsxmslem2  18075  nrgabv  18172  nmvs  18187  nvclvec  18207  nmoge0  18230  nghmcl  18236  nmoi  18237  nghmghm  18243  nmhmlmhm  18258  nmhmnghm  18259  icccmp  18330  xrge0gsumle  18338  xrge0tsms  18339  metds0  18354  metdstri  18355  metdsre  18357  metdseq0  18358  metdscnlem  18359  metnrmlem1a  18362  icopnfcnv  18440  xrhmeo  18444  pcoval1  18511  cphreccllem  18614  cmetcvg  18711  lmle  18727  cmscmet  18768  hlcph  18781  minveclem4  18796  ivthlem3  18813  ovolmge0  18836  ovolicc1  18875  ovolicc2lem3  18878  ovolicc2lem5  18880  mblsplit  18891  dyadmbl  18955  mbfdm  18983  mbfadd  19016  mbfsub  19017  i1ff  19031  i1frn  19032  i1fima2  19034  mbfmul  19081  itg2monolem1  19105  bddmulibl  19193  dvnres  19280  c1liplem1  19343  c1lip2  19345  dvge0  19353  lhop1lem  19360  itgsubstlem  19395  fta1glem1  19551  fta1glem2  19552  fta1b  19555  plyf  19580  plypf1  19594  plyadd  19599  plymul  19600  coeeu  19607  dgrlem  19611  coeid  19620  elqaalem3  19701  aareccl  19706  eff1olem  19910  relogf1o  19924  logdmn0  19987  logcnlem2  19990  logcnlem3  19991  dvloglem  19995  efopnlem1  20003  efopnlem2  20004  logtayl2  20009  cxpcn3lem  20087  cxpcn3  20088  atandmneg  20202  atandmcj  20205  efiatan2  20213  cosatan  20217  cosatanne0  20218  dvatan  20231  areage0  20258  cxp2lim  20271  jensenlem2  20282  jensen  20283  wilthlem1  20306  wilth  20309  ftalem3  20312  efnnfsumcl  20340  isppw  20352  efchtdvds  20397  sqff1o  20420  dvdsdivcl  20421  fsumdvdsdiaglem  20423  dvdsppwf1o  20426  dvdsflf1o  20427  musum  20431  muinv  20433  dvdsmulf1o  20434  fsumvma2  20453  vmasum  20455  chpval2  20457  chpchtsum  20458  chpub  20459  mersenne  20466  perfect1  20467  bposlem1  20523  bposlem5  20527  bposlem6  20528  lgsfle1  20544  lgsle1  20550  lgsdirprm  20568  lgsne0  20572  lgsqrlem4  20583  lgseisenlem3  20590  lgseisenlem4  20591  lgsquadlem1  20593  lgsquadlem2  20594  2sqblem  20616  chebbnd1lem1  20618  chebbnd1  20621  chtppilim  20624  chpchtlim  20628  chpo1ub  20629  rplogsumlem2  20634  rpvmasumlem  20636  dchrmusumlema  20642  dchrvmasumlem1  20644  dchrisum0flblem2  20658  dchrisum0lema  20663  dchrisum0lem2a  20666  logsqvma  20691  selberg3lem2  20707  pntrsumo1  20714  pnt2  20762  ostthlem1  20776  padicabvf  20780  ostth3  20787  gxneg  20933  gxadd  20942  gxmul  20945  ablocom  20952  subgoablo  20978  smgrpisass  21000  mndoisexid  21007  zrdivrng  21099  phpar2  21401  cbncms  21444  hlph  21468  hcaucvg  21765  hlimconvi  21770  shaddcl  21796  shmulcl  21797  shmulclOLD  21798  chlimi  21814  chcompl  21822  choc1  21906  nmopre  22450  cnopc  22493  lnopl  22494  unop  22495  hmop  22502  cnfnc  22510  lnfnl  22511  nlelshi  22640  cnlnadjlem5  22651  elpjidm  22764  mdslle1i  22897  mdslle2i  22898  atcv0  22922  chpssati  22943  ballotlem4  23057  ballotlem5  23058  ballotlemfrc  23085  ballotlemirc  23090  ballotth  23096  fovcld  23203  ofrn  23206  ssnnssfz  23277  tpr2rico  23296  rge0scvg  23373  xrge0tsmsd  23382  rnlogblem  23401  esumpinfval  23441  esumpcvgval  23446  esumpmono  23447  0elsiga  23475  sigaclcu  23478  issgon  23484  sxuni  23524  isrnmeas  23531  measvuni  23542  measssd  23543  imambfm  23567  elmbfmvol2  23572  probtot  23615  eldmgm  23694  dmgmaddn0  23695  subfacp1lem3  23713  subfacp1lem5  23715  pconcn  23755  sconpht  23760  conpcon  23766  cvmcov  23794  cvmliftlem1  23816  cvmliftlem10  23825  cvmlift2lem11  23844  cvmlift2lem12  23845  umgrale  23873  fundmpss  24122  tfisg  24204  wfisg  24209  frinsg  24245  wfrlem5  24260  frrlem5  24285  sltval2  24310  txpss3v  24418  pprodss4v  24424  axcontlem7  24598  axcontlem10  24601  onint1  24888  alneal2  25001  injrec2  25119  surjsec2  25120  dstr  25171  domrancur1b  25200  supdef  25262  dirub  25294  trinv  25395  elcarelcl  25906  fnetg  26274  refssfne  26294  neibastop1  26308  filnetlem3  26329  cover2  26358  indexa  26412  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  totbndss  26501  equivtotbnd  26502  isbnd3  26508  totbndbnd  26513  equivbnd  26514  prdsbnd  26517  prdstotbnd  26518  heibor  26545  crngocom  26626  isfld2  26630  dmncrng  26681  prter2  26749  nacsfg  26780  nacsfix  26787  mzpindd  26824  diophrw  26838  diophrex  26855  rexzrexnn0  26885  pell1234qrdich  26946  rmspecnonsq  26992  rmspecfund  26994  rmspecpos  27001  monotoddzzfi  27027  ltrmxnn0  27036  rmxnn  27038  jm2.23  27089  jm3.1lem2  27111  dnnumch3  27144  lnmlssfg  27178  lnmlmic  27186  frlmsslsp  27248  frlmlbs  27249  f1lindf  27292  lnrlnm  27317  lnr2i  27320  lpirlnr  27321  hbtlem6  27333  hbt  27334  mnccoe  27343  psgnunilem5  27417  cntzsdrg  27510  idomrootle  27511  proot1mul  27515  phisum  27518  proot1hash  27519  deg1mhm  27526  cncmpmax  27703  stoweidlem7  27756  stoweidlem14  27763  stoweidlem16  27765  stoweidlem17  27766  stoweidlem24  27773  stoweidlem31  27780  stoweidlem39  27788  stoweidlem50  27799  stoweidlem57  27806  wallispilem3  27816  2reu1  27964  nfunsnafv  28005  faovcl  28060  mpt2xopn0yelv  28079  usgraedg2  28121  nbgrael  28141  ordelordALT  28301  2uasbanh  28327  ordelordALTVD  28643  bnj642  28777  bnj643  28778  bnj645  28779  bnj707  28784  bnj1379  28863  bnj1538  28887  bnj110  28890  bnj93  28895  bnj906  28962  bnj1006  28991  bnj1110  29012  bnj1121  29015  bnj1172  29031  bnj1204  29042  bnj1321  29057  bnj1364  29058  bnj1398  29064  bnj1450  29080  bnj1312  29088  bnj1501  29097  bnj1523  29101  toycom  29162  lsateln0  29185  lpssat  29203  lssat  29206  oposlem  29373  olop  29404  omllaw  29433  cvlexch1  29518  dihpN  31526  mapdordlem2  31827
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 177  df-an 360
  Copyright terms: Public domain W3C validator