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

Theorem simprbi 462
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 461 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  xornan  1375  sb1  1766  eumo  2269  2eu1OLD  2328  reurmo  3025  pssne  3539  pssn2lp  3544  ssnpss  3546  eldifn  3566  elinel2  3629  rabsnt  4049  eldifsni  4098  unimax  4226  ssintub  4245  moop2  4685  pwssun  4729  weso  4814  opelxp2  4857  eldmeldmressn  5134  wfisg  5402  ordwe  5423  funmo  5585  funopg  5601  funun  5611  fununi  5635  funimaexg  5646  fndm  5661  frn  5720  f1ss  5769  f1ssr  5770  f1ssres  5771  forn  5781  f1f1orn  5810  f1orescnv  5814  f1imacnv  5815  funcocnv2  5823  dffv2  5922  exfo  6027  foelrn  6028  isorel  6205  isoini2  6218  f1ofveu  6273  fovcl  6388  f1opw  6510  onminesb  6616  onminsb  6617  tfis  6672  limomss  6688  nnlim  6696  ssnlim  6701  curry1  6876  curry2  6879  f1o2ndf1  6892  fnwelem  6899  ressuppss  6922  mpt2xopn0yelv  6944  wfrlem5  7025  tz7.48lem  7143  dif20el  7192  oeordi  7273  oeeulem  7287  oeeui  7288  nnawordex  7323  swoer  7376  erdisj  7396  eceqoveq  7453  mapsnconst  7502  ixpn0  7539  resixpfo  7545  boxcutc  7550  sdomnen  7582  en0  7616  en1  7620  domunsncan  7655  fodomr  7706  phplem4  7737  php3  7741  unxpdomlem3  7761  fineqvlem  7769  f1opwfi  7858  fsuppcolem  7894  fsuppco  7895  mapfienlem1  7898  mapfienlem2  7899  supub  7952  suplub  7953  ordtypelem2  7978  ordtypelem3  7979  ordtypelem6  7982  ordtypelem7  7983  wemapso2OLD  8011  wemapso2lem  8012  wdom2d  8040  brwdom3  8042  ixpiunwdom  8051  inf3lem2  8079  inf3lem6  8083  oancom  8101  infdifsn  8106  cantnfp1lem3  8131  cantnflem3  8142  cantnflem4  8143  cantnfp1lem3OLD  8157  cantnflem3OLD  8164  cantnflem4OLD  8165  cantnfOLD  8166  mapfienOLD  8170  oef1o  8173  oef1oOLD  8174  cnfcom3  8180  cnfcomlemOLD  8183  cnfcom3OLD  8188  tctr  8203  tz9.12lem3  8239  scottex  8335  cardid2  8366  infxpenlem  8423  acni3  8460  cardaleph  8502  iscard3  8506  dfac5lem4  8539  dfac5lem5  8540  kmlem1  8562  cofsmo  8681  fin4en1  8721  enfin2i  8733  fin23lem28  8752  fin23lem38  8761  isf32lem6  8770  enfin1ai  8796  isfin1-3  8798  hsmexlem2  8839  hsmexlem4  8841  domtriomlem  8854  axdc2lem  8860  axdc3lem2  8863  ac6num  8891  zorn2lem2  8909  brdom3  8938  alephval2  8979  alephreg  8989  pwcfsdom  8990  smobeth  8993  fpwwe2lem6  9043  fpwwe2lem13  9050  canthp1lem2  9061  pwfseqlem3  9068  hargch  9081  winalim2  9104  gchina  9107  inar1  9183  0npi  9290  mulclpi  9301  mulcanpi  9308  nlt1pi  9314  nqereu  9337  prcdnq  9401  prnmax  9403  ltresr2  9548  axrnegex  9569  axpre-sup  9576  1nuz2  11202  zsupss  11216  rpgt0  11276  ixxss1  11600  ixxss2  11601  ixxss12  11602  lbioo  11613  ubioo  11614  iccss2  11649  iccssico2  11652  elfzuz3  11739  uzdisj  11806  nn0disj  11846  serge0  12205  expge0  12246  expge1  12247  expaddzlem  12253  hashrabsn1  12490  hashfun  12544  relexpuzrel  13034  shftfn  13055  sqrlem6  13230  rlimss  13474  lo1dm  13491  o1dm  13502  rlimrege0  13551  fsumf1o  13694  fsumge0  13760  incexc2  13801  supcvg  13819  fprodf1o  13905  divalglem9  14268  bitsfzolem  14293  bitsinv2  14302  bitsf1ocnv  14303  bitsf1  14305  gcdcllem1  14358  bezout  14389  prmind2  14437  nprm  14440  sqnprm  14448  dvdsprm  14449  coprm  14450  isprm5  14462  phibndlem  14509  dfphi2  14513  phimullem  14518  pclem  14571  pcpre1  14575  pcidlem  14604  expnprm  14630  prmreclem1  14643  prmreclem2  14644  prmreclem5  14647  1arith  14654  4sqlem18  14689  vdwnnlem3  14724  ramtlecl  14727  rami  14742  0ram  14747  ramub1lem1  14753  firest  15047  acsfiel  15268  isacs1i  15271  catlid  15297  catrid  15298  fullfo  15525  fthf1  15530  fthoppc  15536  invfuc  15587  prslem  15884  posi  15903  dlatmjdi  16148  pslem  16160  tsrlin  16173  cnvtsr  16176  tsrdir  16192  mndid  16257  mhmf  16295  mhmlin  16297  mhm0  16298  mrcmndind  16321  grpinvex  16389  grplinv  16420  mulgz  16487  mulgdirlem  16490  mulgdir  16491  mulgass  16496  nsgbi  16556  nmzbi  16565  ghmf  16595  ghmlin  16596  conjnsg  16626  gimf1o  16635  gagrpid  16656  gaf  16657  gaass  16659  psgnunilem5  16843  odid  16886  odf1o2  16917  gexid  16925  sylow1lem4  16945  odcau  16948  pj1id  17041  efgredeu  17094  ablcmn  17128  cmncom  17138  mulgdi  17159  gexexlem  17182  torsubg  17184  cyggenod2  17212  cygctb  17218  ghmcyg  17222  dprdf1o  17399  dprd2dlem1  17410  dprd2da  17411  ablfacrplem  17436  ablfaclem2  17457  ablfac2  17460  crngmgp  17526  rhmmhm  17691  rhmghm  17694  drngunit  17721  drngmgp  17728  drngid  17730  subrgss  17750  subrg1cl  17757  issubdrg  17774  abvge0  17794  srngcnv  17822  lmhmlin  18001  lmimf1o  18029  lvecdrng  18071  lspsolvlem  18108  islbs3  18121  lbsextlem3  18126  2idlcpbl  18202  nzrnz  18228  opprnzr  18233  rrgeq0i  18257  domneq0  18266  domnrrg  18269  drngdomn  18272  fldidom  18274  assalem  18285  mplsubrglem  18420  mplsubrglemOLD  18421  mplcoe1  18447  mplbas2  18454  mplbas2OLD  18455  opsrtoslem2  18469  mplelsfi  18475  mplelsfiOLD  18476  coe1mul2  18630  zringunit  18828  prmirredlem  18830  znidomb  18898  cygzn  18907  psgndiflemB  18934  pjf  19042  frlmsslsp  19123  frlmlbs  19124  f1lindf  19149  pmatcoe1fsupp  19494  toponuni  19720  tpsuni  19731  clsval2  19843  mretopd  19886  neips  19907  neiptoptop  19925  neiptopnei  19926  perflp  19948  perfi  19949  restfpw  19973  cnf  20040  cnpf  20041  cnpimaex  20050  cnima  20059  t0sep  20118  t1sncld  20120  t1ficld  20121  hausnei  20122  regsep  20128  pnrmcld  20136  nrmsep3  20149  cnrmi  20154  cmpcov  20182  discmp  20191  tgcmp  20194  uncmp  20196  hauscmplem  20199  cmpfi  20201  conclo  20208  1stcclb  20237  2ndcdisj  20249  llyi  20267  nllyi  20268  ptpjpre1  20364  ptpjcn  20404  ptpjopn  20405  ptclsg  20408  dfac14  20411  txdis1cn  20428  pthaus  20431  hauseqlcld  20439  txkgen  20445  xkococn  20453  txcon  20482  hmeocnvcn  20554  fbssfi  20630  filss  20646  ufilss  20698  uffixfr  20716  flimneiss  20759  flimelbas  20761  fclscf  20818  flimfnfcls  20821  alexsublem  20836  alexsubb  20838  alexsubALT  20843  ptcmplem2  20845  ptcmplem3  20846  ptcmplem4  20847  tmdgsum2  20887  ghmcnp  20905  tgpt0  20909  qustgplem  20911  tsmsfbas  20918  tsmslem1  20919  tsmsgsum  20929  tsmsgsumOLD  20932  tsmssubm  20936  tsmsresOLD  20937  tsmsres  20938  tsmsf1o  20939  tsmsmhm  20940  tsmsadd  20941  tsmsxplem1  20947  tsmsxplem2  20948  tsmsxp  20949  istdrg2  20972  vscacn  20980  tvctdrg  20987  uspreg  21069  ucncn  21080  neipcfilu  21091  cuspcvg  21096  psmetxrge0  21109  isxmet2d  21122  prdsxmetlem  21163  imasdsf1olem  21168  xmstopn  21246  mstopn  21247  stdbdxmet  21310  prdsxmslem2  21324  nrgabv  21462  nmvs  21477  nvclvec  21497  nmoge0  21520  nghmcl  21526  nmoi  21527  nghmghm  21533  nmhmlmhm  21548  nmhmnghm  21549  icccmp  21622  xrge0gsumle  21630  xrge0tsms  21631  metds0  21646  metdstri  21647  metdsre  21649  metdseq0  21650  metdscnlem  21651  metnrmlem1a  21654  icopnfcnv  21734  xrhmeo  21738  pcoval1  21805  cvslvec  21898  cvsunit  21900  cphreccllem  21917  cmetcvg  22016  lmle  22032  cmscmet  22077  cmetcusp1OLD  22083  cmetcusp1  22084  hlcph  22096  minveclem4  22139  ivthlem3  22157  ovolmge0  22180  ovolicc1  22219  ovolicc2lem3  22222  ovolicc2lem5  22224  mblsplit  22235  dyadmbl  22301  mbfdm  22327  mbfadd  22360  mbfsub  22361  i1ff  22375  i1frn  22376  i1fima2  22378  mbfmul  22425  itg2monolem1  22449  bddmulibl  22537  dvnres  22626  c1liplem1  22689  c1lip2  22691  dvge0  22699  lhop1lem  22706  itgsubstlem  22741  fta1glem1  22858  fta1glem2  22859  fta1b  22862  plyf  22887  plypf1  22901  plyadd  22906  plymul  22907  coeeu  22914  dgrlem  22918  coeid  22927  elqaalem3  23009  aareccl  23014  eff1olem  23227  relogf1o  23246  logdmn0  23315  logcnlem2  23318  logcnlem3  23319  dvloglem  23323  efopnlem1  23331  efopnlem2  23332  logtayl2  23337  cxpcn3lem  23417  cxpcn3  23418  atandmneg  23562  atandmcj  23565  efiatan2  23573  cosatan  23577  cosatanne0  23578  dvatan  23591  areage0  23619  cxp2lim  23632  jensenlem2  23643  jensen  23644  eldmgm  23677  dmgmaddn0  23678  dmlogdmgm  23679  lgamgulmlem2  23685  lgamgulmlem3  23686  lgamgulmlem5  23688  lgambdd  23692  lgamucov  23693  wilthlem1  23723  wilth  23726  ftalem3  23729  efnnfsumcl  23757  isppw  23769  efchtdvds  23814  sqff1o  23837  dvdsdivcl  23838  fsumdvdsdiaglem  23840  dvdsppwf1o  23843  dvdsflf1o  23844  musum  23848  muinv  23850  dvdsmulf1o  23851  fsumvma2  23870  vmasum  23872  chpval2  23874  chpchtsum  23875  chpub  23876  mersenne  23883  perfect1  23884  bposlem1  23940  bposlem5  23944  lgsfle1  23961  lgsle1  23967  lgsdirprm  23985  lgsne0  23989  lgsqrlem4  24000  lgseisenlem3  24007  lgseisenlem4  24008  lgsquadlem1  24010  lgsquadlem2  24011  2sqblem  24033  chebbnd1lem1  24035  chebbnd1  24038  chtppilim  24041  chpchtlim  24045  chpo1ub  24046  rplogsumlem2  24051  rpvmasumlem  24053  dchrmusumlema  24059  dchrvmasumlem1  24061  dchrisum0flblem2  24075  dchrisum0lema  24080  dchrisum0lem2a  24083  logsqvma  24108  selberg3lem2  24124  pntrsumo1  24131  pnt2  24179  ostthlem1  24193  ostth3  24204  axtgcgrrflx  24238  axtgcgrid  24239  axtgsegcon  24240  axtg5seg  24241  axtgbtwnid  24242  axtgpasch  24243  axtgcont1  24244  tglng  24316  axcontlem7  24690  axcontlem10  24693  umgrale  24738  usgraedg2  24792  usgraexmpledg  24820  clwlkfclwwlk1hashn  25258  eupatrl  25385  gxneg  25682  gxadd  25691  gxmul  25694  ablocom  25701  subgoablo  25727  smgrpisass  25749  mndoisexid  25756  zrdivrng  25848  phpar2  26152  cbncms  26195  hlph  26219  hcaucvg  26517  hlimconvi  26522  shaddcl  26548  shmulcl  26549  shmulclOLD  26550  chlimi  26566  chcompl  26574  choc1  26659  nmopre  27202  cnopc  27245  lnopl  27246  unop  27247  hmop  27254  cnfnc  27262  lnfnl  27263  nlelshi  27392  cnlnadjlem5  27403  elpjidm  27516  mdslle1i  27649  mdslle2i  27650  atcv0  27674  chpssati  27695  elin2d  27833  fovcld  27921  aciunf1lem  27946  padct  27992  ssnnssfz  28045  ressprs  28095  oduprs  28096  resspos  28099  resstos  28100  tleile  28101  ogrpinvOLD  28157  ogrpinv0le  28158  ogrpsub  28159  ogrpaddlt  28160  isarchi3  28183  archirng  28184  archirngz  28185  archiabllem1a  28187  archiabllem1b  28188  archiabllem2a  28190  archiabllem2c  28191  archiabllem2b  28192  archiabl  28194  xrge0tsmsd  28228  orngsqr  28247  ornglmulle  28248  orngrmulle  28249  ofldtos  28254  ofldlt1  28256  ofldchr  28257  suborng  28258  subofld  28259  isarchiofld  28260  nn0omnd  28284  qtophaus  28292  crefi  28303  cmpcref  28306  cmppcmp  28314  pcmplfin  28316  tpr2rico  28347  rge0scvg  28384  zrhunitpreima  28411  qqhrhm  28422  esummono  28501  gsumesum  28506  esumrnmpt2  28515  esumpinfval  28520  esumpcvgval  28525  esumpmono  28526  0elsiga  28562  sigaclcu  28565  issgon  28571  inelpisys  28602  ldsysgenld  28608  ldgenpisyslem1  28611  sxuni  28641  isrnmeas  28648  measvuni  28662  measssd  28663  ddemeas  28685  imambfm  28710  elmbfmvol2  28715  dya2icoseg2  28726  omssubaddlem  28747  omssubadd  28748  carsgsigalem  28763  pmeasmono  28772  sibfinima  28787  oddpwdc  28799  oddpwdcv  28800  eulerpartlemf  28815  eulerpartlemt  28816  eulerpartlemr  28819  eulerpartlemgvv  28821  eulerpartlemgs2  28825  sseqf  28837  fiblem  28843  probtot  28857  ballotlem4  28943  ballotlem5  28944  ballotlemfrc  28971  ballotlemirc  28976  ballotth  28982  bnj642  29132  bnj643  29133  bnj645  29134  bnj707  29139  bnj1379  29216  bnj1538  29240  bnj110  29243  bnj93  29248  bnj906  29315  bnj1006  29344  bnj1110  29365  bnj1121  29368  bnj1172  29384  bnj1204  29395  bnj1321  29410  bnj1364  29411  bnj1398  29417  bnj1450  29433  bnj1312  29441  bnj1501  29450  bnj1523  29454  subfacp1lem3  29479  subfacp1lem5  29481  pconcn  29521  sconpht  29526  conpcon  29532  cvmcov  29560  cvmliftlem1  29582  cvmliftlem10  29591  cvmlift2lem11  29610  cvmlift2lem12  29611  msubff1  29768  mvhf1  29771  mthmpps  29794  mclspps  29796  fundmpss  29980  tfisg  30030  frinsg  30056  frrlem5  30091  sltval2  30116  txpss3v  30216  pprodss4v  30222  fnetg  30573  neibastop1  30587  filnetlem3  30608  onint1  30681  bj-elid2  31165  icorempt2  31268  wl-nfeqfb  31357  fin2solem  31411  fin2so  31412  ptrest  31420  mblfinlem2  31424  dvtan  31438  itg2gt0cn  31443  ftc1anclem7  31469  ftc1anclem8  31470  ftc1anc  31471  cover2  31486  indexa  31506  istotbnd3  31549  sstotbnd2  31552  sstotbnd  31553  totbndss  31555  equivtotbnd  31556  isbnd3  31562  totbndbnd  31567  equivbnd  31568  prdsbnd  31571  prdstotbnd  31572  heibor  31599  crngocom  31680  isfld2  31684  dmncrng  31735  prter2  31904  toycom  31991  lsateln0  32013  lpssat  32031  lssat  32034  oposlem  32200  olop  32232  omllaw  32261  cvlexch1  32346  dihpN  34356  mapdordlem2  34657  nacsfg  34999  nacsfix  35006  mzpindd  35040  diophrw  35053  diophrex  35070  rexzrexnn0  35099  pell1234qrdich  35158  rmspecsqrtnq  35203  rmspecnonsq  35204  rmspecfund  35206  rmspecpos  35213  monotoddzzfi  35239  ltrmxnn0  35248  rmxnn  35250  jm2.23  35300  jm3.1lem2  35322  dnnumch3  35355  lnmlssfg  35388  lnmlmic  35396  lnrlnm  35426  lnr2i  35429  lpirlnr  35430  hbtlem6  35442  hbt  35443  mnccoe  35451  cntzsdrg  35515  idomrootle  35516  proot1mul  35520  phisum  35523  proot1hash  35524  deg1mhm  35531  radcnvrat  36043  binomcxplemdvbinom  36106  binomcxplemcvg  36107  binomcxplemnotnn0  36109  ordelordALT  36328  2uasbanh  36358  ordelordALTVD  36698  sumnnodd  37004  stoweidlem7  37157  stoweidlem14  37164  stoweidlem16  37166  stoweidlem24  37174  stoweidlem31  37181  stoweidlem54  37204  wallispilem3  37217  fourierdlem42  37299  fourierdlem48  37305  fourierdlem51  37308  fourierdlem64  37321  fourierdlem76  37333  fourierdlem79  37336  fourierdlem81  37338  fourierdlem87  37344  etransclem28  37413  etransclem32  37417  2reu1  37559  nfunsnafv  37595  faovcl  37653  evendiv2z  37714  oddp1div2z  37715  2dvdseven  37736  2ndvdsodd  37737  perfectALTVlem1  37796  usgra2pth  37983  clintopcllaw  38164  0ringbas  38188  rnghmmgmhm  38211  uzlidlring  38246  rnghmsubcsetclem1  38294  rngccatidALTV  38308  zrinitorngc  38319  zrtermorngc  38320  rhmsubcsetclem1  38340  funcringcsetcALTV2lem7  38361  ringccatidALTV  38371  funcringcsetclem7ALTV  38384  irinitoringc  38388  zrtermoringc  38389  fldhmsubc  38403  fldhmsubcALTV  38422  ssnn0ssfz  38449  el0ldepsnzr  38579  eluz2gt1  38624  regt1loggt0  38667  elbigodm  38686  fllogbd  38691
  Copyright terms: Public domain W3C validator