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  1641  eumo  2196  2eu1  2236  reurmo  2768  pssne  3285  pssn2lp  3290  ssnpss  3292  eldifn  3312  rabsnt  3717  eldifsni  3763  unimax  3877  ssintub  3896  moop2  4277  pwssun  4315  weso  4400  ordwe  4421  reusv6OLD  4561  onminesb  4605  onminsb  4606  tfis  4661  limomss  4677  nnlim  4685  ssnlim  4690  opelxp2  4739  funmo  5287  funopg  5302  funun  5312  fununi  5332  funimaexg  5345  fndm  5359  frn  5411  f1ss  5458  f1ssr  5459  f1ssres  5460  forn  5470  f1f1orn  5499  f1orescnv  5504  f1imacnv  5505  funcocnv2  5514  dffv2  5608  exfo  5694  foelrn  5695  f1fveq  5802  isorel  5839  isoini2  5852  fovcl  5965  f1opw  6088  curry1  6226  curry2  6229  fnwelem  6246  f1ofveu  6355  tz7.48lem  6469  dif20el  6520  oeordi  6601  oeeulem  6615  oeeui  6616  nnawordex  6651  swoer  6704  erdisj  6723  eceqoveq  6779  mapsnconst  6829  ixpn0  6864  resixpfo  6870  boxcutc  6875  sdomnen  6906  en0  6940  en1  6944  domunsncan  6978  fodomr  7028  phplem4  7059  php3  7063  unxpdomlem3  7085  fineqvlem  7093  suppfif1  7165  f1opwfi  7175  supub  7226  suplub  7227  ordtypelem2  7250  ordtypelem3  7251  ordtypelem6  7254  ordtypelem7  7255  wemapso2  7283  wdom2d  7310  brwdom3  7312  ixpiunwdom  7321  inf3lem2  7346  inf3lem6  7350  oancom  7368  infdifsn  7373  cantnfp1lem3  7398  cantnflem3  7409  cantnflem4  7410  cantnf  7411  mapfien  7415  oef1o  7417  cnfcomlem  7418  cnfcom3  7423  tctr  7441  tz9.12lem3  7477  scottex  7571  cardid2  7602  infxpenlem  7657  acni3  7690  cardaleph  7732  iscard3  7736  dfac5lem4  7769  dfac5lem5  7770  kmlem1  7792  cofsmo  7911  fin4en1  7951  enfin2i  7963  fin23lem28  7982  fin23lem38  7991  isf32lem6  8000  enfin1ai  8026  isfin1-3  8028  hsmexlem2  8069  hsmexlem4  8071  domtriomlem  8084  axdc2lem  8090  axdc3lem2  8093  ac6num  8122  zorn2lem2  8140  brdom3  8169  alephval2  8210  alephreg  8220  pwcfsdom  8221  smobeth  8224  fpwwe2lem6  8273  fpwwe2lem13  8280  canthp1lem2  8291  pwfseqlem3  8298  hargch  8315  winalim2  8334  gchina  8337  inar1  8413  0npi  8522  mulclpi  8533  mulcanpi  8540  nlt1pi  8546  nqereu  8569  enqeq  8574  prcdnq  8633  prnmax  8635  ltresr2  8779  axrnegex  8800  axpre-sup  8807  1nuz2  10309  zsupss  10323  rpgt0  10381  ixxss1  10690  ixxss2  10691  ixxss12  10692  lbioo  10703  ubioo  10704  iccss2  10736  iccssico2  10739  elfzuz3  10811  uzdisj  10872  serge0  11116  expge0  11154  expge1  11155  expaddzlem  11161  hashfun  11405  shftfn  11584  sqrlem6  11749  eqsqrd  11867  rlimss  11992  lo1dm  12009  o1dm  12020  rlimrege0  12069  fsumf1o  12212  fsumge0  12269  incexc2  12313  supcvg  12330  divalglem9  12616  bitsfzolem  12641  bitsinv2  12650  bitsf1ocnv  12651  bitsf1  12653  gcdcllem1  12706  bezout  12737  prmind2  12785  nprm  12788  sqnprm  12793  dvdsprm  12794  coprm  12795  isprm5  12807  prmexpb  12812  phibndlem  12854  dfphi2  12858  phimullem  12863  pclem  12907  pcpre1  12911  pcidlem  12940  pcmpt  12956  expnprm  12966  prmreclem1  12979  prmreclem2  12980  prmreclem5  12983  1arith  12990  4sqlem18  13025  vdwnnlem3  13060  ramtlecl  13063  rami  13078  0ram  13083  ramub1lem1  13089  firest  13353  acsfiel  13572  isacs1i  13575  catlid  13601  catrid  13602  fullfo  13802  fthf1  13807  fthoppc  13813  invfuc  13864  prslem  14081  posi  14100  latlem  14170  clatlem  14232  dlatmjdi  14313  pslem  14331  tsrlin  14344  cnvtsr  14347  tsrdir  14376  mndid  14390  mhmf  14436  mhmlin  14438  mhm0  14439  grpinvex  14513  grplinv  14544  mulgz  14604  mulgdirlem  14607  mulgdir  14608  mulgass  14613  nsgbi  14664  nmzbi  14673  ghmf  14703  ghmlin  14704  conjnsg  14734  gimf1o  14743  gagrpid  14764  gaf  14765  gaass  14767  odid  14869  odf1o2  14900  gexid  14908  sylow1lem4  14928  odcau  14931  pj1id  15024  efgredeu  15077  efgred2  15078  ablcmn  15111  cmncom  15121  mulgdi  15142  gexexlem  15160  torsubg  15162  frgpnabllem2  15178  cyggenod2  15188  cygctb  15194  ghmcyg  15198  dprdf1o  15283  dprd2dlem1  15292  dprd2da  15293  ablfacrplem  15316  ablfaclem2  15337  ablfac2  15340  crngmgp  15365  rhmmhm  15518  rhmghm  15519  drngunit  15533  drngmgp  15540  drngid  15542  subrgss  15562  subrg1cl  15569  issubdrg  15586  abvge0  15606  srngcnv  15634  lmhmlin  15808  lmimf1o  15832  lvecdrng  15874  lspsolvlem  15911  islbs3  15924  lbsextlem3  15929  2idlcpbl  16002  nzrnz  16028  opprnzr  16032  rrgeq0i  16046  domneq0  16054  domnrrg  16057  drngdomn  16060  fldidom  16062  assalem  16073  mplsubrglem  16199  mplcoe1  16225  mplbas2  16228  opsrtoslem2  16242  mplelsfi  16248  coe1mul2  16362  zrngunit  16454  prmirredlem  16462  znidomb  16531  cygzn  16540  frgpcyg  16543  pjf  16629  toponuni  16681  tpsuni  16692  clsval2  16803  mretopd  16845  neips  16866  perflp  16901  perfi  16902  restfpw  16926  cnf  16992  cnpf  16993  cnpimaex  17002  cnima  17010  t0sep  17068  t1sncld  17070  t1ficld  17071  hausnei  17072  regsep  17078  pnrmcld  17086  nrmsep3  17099  cnrmi  17104  cmpcov  17132  discmp  17141  tgcmp  17144  uncmp  17146  hauscmplem  17149  cmpfi  17151  conclo  17157  1stcclb  17186  2ndcdisj  17198  llyi  17216  nllyi  17217  ptpjpre1  17282  ptpjcn  17321  ptpjopn  17322  ptclsg  17325  dfac14  17328  txdis1cn  17345  pthaus  17348  hauseqlcld  17356  txkgen  17362  xkococn  17370  txcon  17399  hmeocnvcn  17468  qtophmeo  17524  fbssfi  17548  filss  17564  ufilss  17616  uffixfr  17634  flimneiss  17677  flimelbas  17679  fclscf  17736  flimfnfcls  17739  alexsublem  17754  alexsubb  17756  alexsubALT  17761  ptcmplem2  17763  ptcmplem3  17764  ptcmplem4  17765  tmdgsum2  17795  ghmcnp  17813  tgpt0  17817  divstgplem  17819  tsmsfbas  17826  tsmslem1  17827  tsmsgsum  17837  tsmssubm  17841  tsmsres  17842  tsmsf1o  17843  tsmsmhm  17844  tsmsadd  17845  tsmsxplem1  17851  tsmsxplem2  17852  tsmsxp  17853  istdrg2  17876  vscacn  17884  tvctdrg  17891  isxmet2d  17908  prdsxmetlem  17948  imasdsf1olem  17953  xmstopn  18013  mstopn  18014  stdbdxmet  18077  prdsxmslem2  18091  nrgabv  18188  nmvs  18203  nvclvec  18223  nmoge0  18246  nghmcl  18252  nmoi  18253  nghmghm  18259  nmhmlmhm  18274  nmhmnghm  18275  icccmp  18346  xrge0gsumle  18354  xrge0tsms  18355  metds0  18370  metdstri  18371  metdsre  18373  metdseq0  18374  metdscnlem  18375  metnrmlem1a  18378  icopnfcnv  18456  xrhmeo  18460  pcoval1  18527  cphreccllem  18630  cmetcvg  18727  lmle  18743  cmscmet  18784  hlcph  18797  minveclem4  18812  ivthlem3  18829  ovolmge0  18852  ovolicc1  18891  ovolicc2lem3  18894  ovolicc2lem5  18896  mblsplit  18907  dyadmbl  18971  mbfdm  18999  mbfadd  19032  mbfsub  19033  i1ff  19047  i1frn  19048  i1fima2  19050  mbfmul  19097  itg2monolem1  19121  bddmulibl  19209  dvnres  19296  c1liplem1  19359  c1lip2  19361  dvge0  19369  lhop1lem  19376  itgsubstlem  19411  fta1glem1  19567  fta1glem2  19568  fta1b  19571  plyf  19596  plypf1  19610  plyadd  19615  plymul  19616  coeeu  19623  dgrlem  19627  coeid  19636  elqaalem3  19717  aareccl  19722  eff1olem  19926  relogf1o  19940  logdmn0  20003  logcnlem2  20006  logcnlem3  20007  dvloglem  20011  efopnlem1  20019  efopnlem2  20020  logtayl2  20025  cxpcn3lem  20103  cxpcn3  20104  atandmneg  20218  atandmcj  20221  efiatan2  20229  cosatan  20233  cosatanne0  20234  dvatan  20247  areage0  20274  cxp2lim  20287  jensenlem2  20298  jensen  20299  wilthlem1  20322  wilth  20325  ftalem3  20328  efnnfsumcl  20356  isppw  20368  efchtdvds  20413  sqff1o  20436  dvdsdivcl  20437  fsumdvdsdiaglem  20439  dvdsppwf1o  20442  dvdsflf1o  20443  musum  20447  muinv  20449  dvdsmulf1o  20450  fsumvma2  20469  vmasum  20471  chpval2  20473  chpchtsum  20474  chpub  20475  mersenne  20482  perfect1  20483  bposlem1  20539  bposlem5  20543  bposlem6  20544  lgsfle1  20560  lgsle1  20566  lgsdirprm  20584  lgsne0  20588  lgsqrlem4  20599  lgseisenlem3  20606  lgseisenlem4  20607  lgsquadlem1  20609  lgsquadlem2  20610  2sqblem  20632  chebbnd1lem1  20634  chebbnd1  20637  chtppilim  20640  chpchtlim  20644  chpo1ub  20645  rplogsumlem2  20650  rpvmasumlem  20652  dchrmusumlema  20658  dchrvmasumlem1  20660  dchrisum0flblem2  20674  dchrisum0lema  20679  dchrisum0lem2a  20682  logsqvma  20707  selberg3lem2  20723  pntrsumo1  20730  pnt2  20778  ostthlem1  20792  padicabvf  20796  ostth3  20803  gxneg  20949  gxadd  20958  gxmul  20961  ablocom  20968  subgoablo  20994  smgrpisass  21016  mndoisexid  21023  zrdivrng  21115  phpar2  21417  cbncms  21460  hlph  21484  hcaucvg  21781  hlimconvi  21786  shaddcl  21812  shmulcl  21813  shmulclOLD  21814  chlimi  21830  chcompl  21838  choc1  21922  nmopre  22466  cnopc  22509  lnopl  22510  unop  22511  hmop  22518  cnfnc  22526  lnfnl  22527  nlelshi  22656  cnlnadjlem5  22667  elpjidm  22780  mdslle1i  22913  mdslle2i  22914  atcv0  22938  chpssati  22959  ballotlem4  23073  ballotlem5  23074  ballotlemfrc  23101  ballotlemirc  23106  ballotth  23112  fovcld  23218  ofrn  23221  ssnnssfz  23292  tpr2rico  23311  rge0scvg  23388  xrge0tsmsd  23397  rnlogblem  23416  esumpinfval  23456  esumpcvgval  23461  esumpmono  23462  0elsiga  23490  sigaclcu  23493  issgon  23499  sxuni  23539  isrnmeas  23546  measvuni  23557  measssd  23558  imambfm  23582  elmbfmvol2  23587  probtot  23630  eldmgm  23709  dmgmaddn0  23710  subfacp1lem3  23728  subfacp1lem5  23730  pconcn  23770  sconpht  23775  conpcon  23781  cvmcov  23809  cvmliftlem1  23831  cvmliftlem10  23840  cvmlift2lem11  23859  cvmlift2lem12  23860  umgrale  23888  fprodf1o  24172  fundmpss  24193  tfisg  24275  wfisg  24280  frinsg  24316  wfrlem5  24331  frrlem5  24356  sltval2  24381  txpss3v  24489  pprodss4v  24495  axcontlem7  24670  axcontlem10  24673  onint1  24960  itg2gt0cn  25006  alneal2  25104  injrec2  25222  surjsec2  25223  dstr  25274  domrancur1b  25303  supdef  25365  dirub  25397  trinv  25498  elcarelcl  26009  fnetg  26377  refssfne  26397  neibastop1  26411  filnetlem3  26432  cover2  26461  indexa  26515  istotbnd3  26598  sstotbnd2  26601  sstotbnd  26602  totbndss  26604  equivtotbnd  26605  isbnd3  26611  totbndbnd  26616  equivbnd  26617  prdsbnd  26620  prdstotbnd  26621  heibor  26648  crngocom  26729  isfld2  26733  dmncrng  26784  prter2  26852  nacsfg  26883  nacsfix  26890  mzpindd  26927  diophrw  26941  diophrex  26958  rexzrexnn0  26988  pell1234qrdich  27049  rmspecnonsq  27095  rmspecfund  27097  rmspecpos  27104  monotoddzzfi  27130  ltrmxnn0  27139  rmxnn  27141  jm2.23  27192  jm3.1lem2  27214  dnnumch3  27247  lnmlssfg  27281  lnmlmic  27289  frlmsslsp  27351  frlmlbs  27352  f1lindf  27395  lnrlnm  27420  lnr2i  27423  lpirlnr  27424  hbtlem6  27436  hbt  27437  mnccoe  27446  psgnunilem5  27520  cntzsdrg  27613  idomrootle  27614  proot1mul  27618  phisum  27621  proot1hash  27622  deg1mhm  27629  cncmpmax  27806  stoweidlem7  27859  stoweidlem14  27866  stoweidlem16  27868  stoweidlem17  27869  stoweidlem24  27876  stoweidlem31  27883  stoweidlem39  27891  stoweidlem50  27902  stoweidlem57  27909  wallispilem3  27919  2reu1  28067  nfunsnafv  28110  faovcl  28168  mpt2xopn0yelv  28195  usgraedg2  28255  nbgrael  28275  eupatrl  28385  ordelordALT  28600  2uasbanh  28626  ordelordALTVD  28959  bnj642  29093  bnj643  29094  bnj645  29095  bnj707  29100  bnj1379  29179  bnj1538  29203  bnj110  29206  bnj93  29211  bnj906  29278  bnj1006  29307  bnj1110  29328  bnj1121  29331  bnj1172  29347  bnj1204  29358  bnj1321  29373  bnj1364  29374  bnj1398  29380  bnj1450  29396  bnj1312  29404  bnj1501  29413  bnj1523  29417  toycom  29784  lsateln0  29807  lpssat  29825  lssat  29828  oposlem  29995  olop  30026  omllaw  30055  cvlexch1  30140  dihpN  32148  mapdordlem2  32449
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