MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprbi Structured version   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  2321  2eu1  2361  reurmo  2923  pssne  3443  pssn2lp  3448  ssnpss  3450  eldifn  3470  rabsnt  3881  eldifsni  3928  unimax  4049  ssintub  4068  moop2  4451  pwssun  4489  weso  4573  ordwe  4594  reusv6OLD  4734  onminesb  4778  onminsb  4779  tfis  4834  limomss  4850  nnlim  4858  ssnlim  4863  opelxp2  4912  funmo  5470  funopg  5485  funun  5495  fununi  5517  funimaexg  5530  fndm  5544  frn  5597  f1ss  5644  f1ssr  5645  f1ssres  5646  forn  5656  f1f1orn  5685  f1orescnv  5690  f1imacnv  5691  funcocnv2  5700  dffv2  5796  exfo  5887  foelrn  5888  isorel  6046  isoini2  6059  fovcl  6175  f1opw  6299  curry1  6438  curry2  6441  f1o2ndf1  6454  fnwelem  6461  mpt2xopn0yelv  6464  f1ofveu  6584  tz7.48lem  6698  dif20el  6749  oeordi  6830  oeeulem  6844  oeeui  6845  nnawordex  6880  swoer  6933  erdisj  6952  eceqoveq  7009  mapsnconst  7059  ixpn0  7094  resixpfo  7100  boxcutc  7105  sdomnen  7136  en0  7170  en1  7174  domunsncan  7208  fodomr  7258  phplem4  7289  php3  7293  unxpdomlem3  7315  fineqvlem  7323  suppfif1  7400  f1opwfi  7410  supub  7464  suplub  7465  ordtypelem2  7488  ordtypelem3  7489  ordtypelem6  7492  ordtypelem7  7493  wemapso2  7521  wdom2d  7548  brwdom3  7550  ixpiunwdom  7559  inf3lem2  7584  inf3lem6  7588  oancom  7606  infdifsn  7611  cantnfp1lem3  7636  cantnflem3  7647  cantnflem4  7648  cantnf  7649  mapfien  7653  oef1o  7655  cnfcomlem  7656  cnfcom3  7661  tctr  7679  tz9.12lem3  7715  scottex  7809  cardid2  7840  infxpenlem  7895  acni3  7928  cardaleph  7970  iscard3  7974  dfac5lem4  8007  dfac5lem5  8008  kmlem1  8030  cofsmo  8149  fin4en1  8189  enfin2i  8201  fin23lem28  8220  fin23lem38  8229  isf32lem6  8238  enfin1ai  8264  isfin1-3  8266  hsmexlem2  8307  hsmexlem4  8309  domtriomlem  8322  axdc2lem  8328  axdc3lem2  8331  ac6num  8359  zorn2lem2  8377  brdom3  8406  alephval2  8447  alephreg  8457  pwcfsdom  8458  smobeth  8461  fpwwe2lem6  8510  fpwwe2lem13  8517  canthp1lem2  8528  pwfseqlem3  8535  hargch  8552  winalim2  8571  gchina  8574  inar1  8650  0npi  8759  mulclpi  8770  mulcanpi  8777  nlt1pi  8783  nqereu  8806  prcdnq  8870  prnmax  8872  ltresr2  9016  axrnegex  9037  axpre-sup  9044  1nuz2  10551  zsupss  10565  rpgt0  10623  ixxss1  10934  ixxss2  10935  ixxss12  10936  lbioo  10947  ubioo  10948  iccss2  10981  iccssico2  10984  elfzuz3  11056  uzdisj  11119  serge0  11377  expge0  11416  expge1  11417  expaddzlem  11423  hashfun  11700  shftfn  11888  sqrlem6  12053  rlimss  12296  lo1dm  12313  o1dm  12324  rlimrege0  12373  fsumf1o  12517  fsumge0  12574  incexc2  12618  supcvg  12635  divalglem9  12921  bitsfzolem  12946  bitsinv2  12955  bitsf1ocnv  12956  bitsf1  12958  gcdcllem1  13011  bezout  13042  prmind2  13090  nprm  13093  sqnprm  13098  dvdsprm  13099  coprm  13100  isprm5  13112  prmexpb  13117  phibndlem  13159  dfphi2  13163  phimullem  13168  pclem  13212  pcpre1  13216  pcidlem  13245  pcmpt  13261  expnprm  13271  prmreclem1  13284  prmreclem2  13285  prmreclem5  13288  1arith  13295  4sqlem18  13330  vdwnnlem3  13365  ramtlecl  13368  rami  13383  0ram  13388  ramub1lem1  13394  firest  13660  acsfiel  13879  isacs1i  13882  catlid  13908  catrid  13909  fullfo  14109  fthf1  14114  fthoppc  14120  invfuc  14171  prslem  14388  posi  14407  latlem  14477  clatlem  14539  dlatmjdi  14620  pslem  14638  tsrlin  14651  cnvtsr  14654  tsrdir  14683  mndid  14697  mhmf  14743  mhmlin  14745  mhm0  14746  grpinvex  14820  grplinv  14851  mulgz  14911  mulgdirlem  14914  mulgdir  14915  mulgass  14920  nsgbi  14971  nmzbi  14980  ghmf  15010  ghmlin  15011  conjnsg  15041  gimf1o  15050  gagrpid  15071  gaf  15072  gaass  15074  odid  15176  odf1o2  15207  gexid  15215  sylow1lem4  15235  odcau  15238  pj1id  15331  efgredeu  15384  ablcmn  15418  cmncom  15428  mulgdi  15449  gexexlem  15467  torsubg  15469  cyggenod2  15495  cygctb  15501  ghmcyg  15505  dprdf1o  15590  dprd2dlem1  15599  dprd2da  15600  ablfacrplem  15623  ablfaclem2  15644  ablfac2  15647  crngmgp  15672  rhmmhm  15825  rhmghm  15826  drngunit  15840  drngmgp  15847  drngid  15849  subrgss  15869  subrg1cl  15876  issubdrg  15893  abvge0  15913  srngcnv  15941  lmhmlin  16111  lmimf1o  16135  lvecdrng  16177  lspsolvlem  16214  islbs3  16227  lbsextlem3  16232  2idlcpbl  16305  nzrnz  16331  opprnzr  16335  rrgeq0i  16349  domneq0  16357  domnrrg  16360  drngdomn  16363  fldidom  16365  assalem  16376  mplsubrglem  16502  mplcoe1  16528  mplbas2  16531  opsrtoslem2  16545  mplelsfi  16551  coe1mul2  16662  zrngunit  16765  prmirredlem  16773  znidomb  16842  cygzn  16851  pjf  16940  toponuni  16992  tpsuni  17003  clsval2  17114  mretopd  17156  neips  17177  neiptoptop  17195  neiptopnei  17196  perflp  17218  perfi  17219  restfpw  17243  cnf  17310  cnpf  17311  cnpimaex  17320  cnima  17329  t0sep  17388  t1sncld  17390  t1ficld  17391  hausnei  17392  regsep  17398  pnrmcld  17406  nrmsep3  17419  cnrmi  17424  cmpcov  17452  discmp  17461  tgcmp  17464  uncmp  17466  hauscmplem  17469  cmpfi  17471  conclo  17478  1stcclb  17507  2ndcdisj  17519  llyi  17537  nllyi  17538  ptpjpre1  17603  ptpjcn  17643  ptpjopn  17644  ptclsg  17647  dfac14  17650  txdis1cn  17667  pthaus  17670  hauseqlcld  17678  txkgen  17684  xkococn  17692  txcon  17721  hmeocnvcn  17793  fbssfi  17869  filss  17885  ufilss  17937  uffixfr  17955  flimneiss  17998  flimelbas  18000  fclscf  18057  flimfnfcls  18060  alexsublem  18075  alexsubb  18077  alexsubALT  18082  ptcmplem2  18084  ptcmplem3  18085  ptcmplem4  18086  tmdgsum2  18126  ghmcnp  18144  tgpt0  18148  divstgplem  18150  tsmsfbas  18157  tsmslem1  18158  tsmsgsum  18168  tsmssubm  18172  tsmsres  18173  tsmsf1o  18174  tsmsmhm  18175  tsmsadd  18176  tsmsxplem1  18182  tsmsxplem2  18183  tsmsxp  18184  istdrg2  18207  vscacn  18215  tvctdrg  18222  uspreg  18304  ucncn  18315  neipcfilu  18326  cuspcvg  18331  psmetxrge0  18344  isxmet2d  18357  prdsxmetlem  18398  imasdsf1olem  18403  xmstopn  18481  mstopn  18482  stdbdxmet  18545  prdsxmslem2  18559  nrgabv  18697  nmvs  18712  nvclvec  18732  nmoge0  18755  nghmcl  18761  nmoi  18762  nghmghm  18768  nmhmlmhm  18783  nmhmnghm  18784  icccmp  18856  xrge0gsumle  18864  xrge0tsms  18865  metds0  18880  metdstri  18881  metdsre  18883  metdseq0  18884  metdscnlem  18885  metnrmlem1a  18888  icopnfcnv  18967  xrhmeo  18971  pcoval1  19038  cphreccllem  19141  cmetcvg  19238  lmle  19254  cmscmet  19299  cmetcusp1OLD  19305  cmetcusp1  19306  hlcph  19318  minveclem4  19333  ivthlem3  19350  ovolmge0  19373  ovolicc1  19412  ovolicc2lem3  19415  ovolicc2lem5  19417  mblsplit  19428  dyadmbl  19492  mbfdm  19520  mbfadd  19553  mbfsub  19554  i1ff  19568  i1frn  19569  i1fima2  19571  mbfmul  19618  itg2monolem1  19642  bddmulibl  19730  dvnres  19817  c1liplem1  19880  c1lip2  19882  dvge0  19890  lhop1lem  19897  itgsubstlem  19932  fta1glem1  20088  fta1glem2  20089  fta1b  20092  plyf  20117  plypf1  20131  plyadd  20136  plymul  20137  coeeu  20144  dgrlem  20148  coeid  20157  elqaalem3  20238  aareccl  20243  eff1olem  20450  relogf1o  20464  logdmn0  20531  logcnlem2  20534  logcnlem3  20535  dvloglem  20539  efopnlem1  20547  efopnlem2  20548  logtayl2  20553  cxpcn3lem  20631  cxpcn3  20632  atandmneg  20746  atandmcj  20749  efiatan2  20757  cosatan  20761  cosatanne0  20762  dvatan  20775  areage0  20802  cxp2lim  20815  jensenlem2  20826  jensen  20827  wilthlem1  20851  wilth  20854  ftalem3  20857  efnnfsumcl  20885  isppw  20897  efchtdvds  20942  sqff1o  20965  dvdsdivcl  20966  fsumdvdsdiaglem  20968  dvdsppwf1o  20971  dvdsflf1o  20972  musum  20976  muinv  20978  dvdsmulf1o  20979  fsumvma2  20998  vmasum  21000  chpval2  21002  chpchtsum  21003  chpub  21004  mersenne  21011  perfect1  21012  bposlem1  21068  bposlem5  21072  bposlem6  21073  lgsfle1  21089  lgsle1  21095  lgsdirprm  21113  lgsne0  21117  lgsqrlem4  21128  lgseisenlem3  21135  lgseisenlem4  21136  lgsquadlem1  21138  lgsquadlem2  21139  2sqblem  21161  chebbnd1lem1  21163  chebbnd1  21166  chtppilim  21169  chpchtlim  21173  chpo1ub  21174  rplogsumlem2  21179  rpvmasumlem  21181  dchrmusumlema  21187  dchrvmasumlem1  21189  dchrisum0flblem2  21203  dchrisum0lema  21208  dchrisum0lem2a  21211  logsqvma  21236  selberg3lem2  21252  pntrsumo1  21259  pnt2  21307  ostthlem1  21321  padicabvf  21325  ostth3  21332  umgrale  21356  usgraedg2  21395  eupatrl  21690  gxneg  21854  gxadd  21863  gxmul  21866  ablocom  21873  subgoablo  21899  smgrpisass  21921  mndoisexid  21928  zrdivrng  22020  phpar2  22324  cbncms  22367  hlph  22391  hcaucvg  22688  hlimconvi  22693  shaddcl  22719  shmulcl  22720  shmulclOLD  22721  chlimi  22737  chcompl  22745  choc1  22829  nmopre  23373  cnopc  23416  lnopl  23417  unop  23418  hmop  23425  cnfnc  23433  lnfnl  23434  nlelshi  23563  cnlnadjlem5  23574  elpjidm  23687  mdslle1i  23820  mdslle2i  23821  atcv0  23845  chpssati  23866  fovcld  24050  ofrn  24052  ssnnssfz  24148  resspos  24187  resstos  24188  tleile  24189  xrge0tsmsd  24223  ofldaddlt  24241  ofld0le1  24242  subofld  24245  kerf1hrm  24262  tpr2rico  24310  rge0scvg  24335  zrhunitpreima  24362  qqhrhm  24373  esummono  24450  gsumesum  24451  esumpinfval  24463  esumpcvgval  24468  esumpmono  24469  0elsiga  24497  sigaclcu  24500  issgon  24506  sxuni  24547  isrnmeas  24554  measvuni  24568  measssd  24569  imambfm  24612  elmbfmvol2  24617  dya2icoseg2  24628  probtot  24670  ballotlem4  24756  ballotlem5  24757  ballotlemfrc  24784  ballotlemirc  24789  ballotth  24795  eldmgm  24806  dmgmaddn0  24807  dmlogdmgm  24808  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamgulmlem5  24817  lgambdd  24821  lgamucov  24822  subfacp1lem3  24868  subfacp1lem5  24870  pconcn  24911  sconpht  24916  conpcon  24922  cvmcov  24950  cvmliftlem1  24972  cvmliftlem10  24981  cvmlift2lem11  25000  cvmlift2lem12  25001  fprodf1o  25272  fundmpss  25390  tfisg  25479  wfisg  25484  frinsg  25520  wfrlem5  25542  frrlem5  25586  sltval2  25611  txpss3v  25723  pprodss4v  25729  axcontlem7  25909  axcontlem10  25912  onint1  26199  mblfinlem2  26244  itg2gt0cn  26260  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  fnetg  26354  refssfne  26374  neibastop1  26388  filnetlem3  26409  cover2  26415  indexa  26435  istotbnd3  26480  sstotbnd2  26483  sstotbnd  26484  totbndss  26486  equivtotbnd  26487  isbnd3  26493  totbndbnd  26498  equivbnd  26499  prdsbnd  26502  prdstotbnd  26503  heibor  26530  crngocom  26611  isfld2  26615  dmncrng  26666  prter2  26730  nacsfg  26759  nacsfix  26766  mzpindd  26803  diophrw  26817  diophrex  26834  rexzrexnn0  26864  pell1234qrdich  26924  rmspecnonsq  26970  rmspecfund  26972  rmspecpos  26979  monotoddzzfi  27005  ltrmxnn0  27014  rmxnn  27016  jm2.23  27067  jm3.1lem2  27089  dnnumch3  27122  lnmlssfg  27155  lnmlmic  27163  frlmsslsp  27225  frlmlbs  27226  f1lindf  27269  lnrlnm  27294  lnr2i  27297  lpirlnr  27298  hbtlem6  27310  hbt  27311  mnccoe  27320  psgnunilem5  27394  cntzsdrg  27487  idomrootle  27488  proot1mul  27492  phisum  27495  proot1hash  27496  deg1mhm  27503  stoweidlem7  27732  stoweidlem14  27739  stoweidlem16  27741  stoweidlem24  27749  stoweidlem31  27756  stoweidlem39  27764  stoweidlem50  27775  stoweidlem54  27779  stoweidlem57  27782  wallispilem3  27792  2reu1  27940  nfunsnafv  27982  faovcl  28040  usgra2pth  28311  ordelordALT  28622  2uasbanh  28648  ordelordALTVD  28979  bnj642  29116  bnj643  29117  bnj645  29118  bnj707  29123  bnj1379  29202  bnj1538  29226  bnj110  29229  bnj93  29234  bnj906  29301  bnj1006  29330  bnj1110  29351  bnj1121  29354  bnj1172  29370  bnj1204  29381  bnj1321  29396  bnj1364  29397  bnj1398  29403  bnj1450  29419  bnj1312  29427  bnj1501  29436  bnj1523  29440  toycom  29770  lsateln0  29793  lpssat  29811  lssat  29814  oposlem  29981  olop  30012  omllaw  30041  cvlexch1  30126  dihpN  32134  mapdordlem2  32435
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