Theorem simprbi 275

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

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpi 120	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simprd 114	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.63dc  954  sb1  1814  reurmo  2753  eldifn  3330  elinel2  3394  rabsnt  3746  eldifsni  3802  unimax  3927  ssintub  3946  exmidsssnc  4293  moop2  4344  wepo  4456  wetrep  4457  trssord  4477  ordelord  4478  ordsucim  4598  ordtri2or2exmidlem  4624  regexmidlem1  4631  reg2exmidlema  4632  tfis  4681  opelxp2  4760  funmo  5341  funopg  5360  funco  5366  funun  5371  fununi  5398  funimaexglem  5413  fndm  5429  frn  5491  f1ss  5548  f1ssr  5549  f1ssres  5551  forn  5562  f1f1orn  5594  f1orescnv  5599  f1imacnv  5600  funcocnv2  5608  funfveu  5652  nfvres  5675  isorel  5949  isoini2  5960  f1ofveu  6006  fovcld  6126  f1opw  6230  f1o2ndf1  6393  mpoxopn0yelv  6405  swoer  6730  mapsnconst  6863  en0  6969  en1  6973  phplem4  7041  phplem4dom  7048  phplem4on  7054  ssfilem  7062  ssfilemd  7064  diffitest  7076  inffiexmid  7098  supubti  7198  suplubti  7199  djuinr  7262  casefun  7284  casef1  7289  djufun  7303  nnnninfeq  7327  ctssexmid  7349  exmidonfinlem  7404  exmidfodomrlemim  7412  cc4f  7488  cc4n  7490  0npi  7533  mulclpi  7548  mulcanpig  7555  nlt1pig  7561  indpi  7562  nnppipi  7563  dfplpq2  7574  archnqq  7637  enq0tr  7654  nqnq0pi  7658  ltexprlemopl  7821  ltexprlemopu  7823  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemupu  7920  caucvgprprlemdisj  7922  suplocsrlempr  8027  ltresr2  8060  peano2nnnn  8073  axrnegex  8099  ltxrlt  8245  peano2nn  9155  elnn0z  9492  zaddcl  9519  ztri3or0  9521  eluz2gt1  9836  1nuz2  9840  rpgt0  9900  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  iccssico2  10182  elfzuz3  10257  uzdisj  10328  nn0disj  10373  zsupcllemstep  10490  zsupssdc  10499  addmodlteq  10661  expge0  10838  expge1  10839  expaddzaplem  10845  shftfn  11402  fsumf1o  11969  fsumge0  12038  fprodf1o  12167  bitsfzolem  12533  bezoutlemzz  12591  bezoutlemaz  12592  bezoutlembz  12593  bezoutlemsup  12598  1nprm  12704  nprm  12713  sqnprm  12726  dvdsprm  12727  coprm  12734  sqpweven  12765  2sqpwodd  12766  dfphi2  12810  phimullem  12815  eulerthlemrprm  12819  phisum  12831  expnprm  12944  1arith  12958  4sqlem18  12999  oddennn  13031  znnen  13037  ennnfonelemg  13042  ctinf  13069  mndid  13526  mhmf  13566  mhmlin  13568  mhm0  13569  grpinvex  13611  grplinv  13651  mulgz  13755  mulgdirlem  13758  mulgdir  13759  mulgass  13764  nsgbi  13809  nmzbi  13814  ghmf  13852  ghmlin  13853  conjnsg  13886  ablcmn  13896  cmncom  13907  crngmgp  14036  rhmmhm  14192  rhmghm  14195  rimf1o  14203  nzrnz  14215  subrgss  14255  subrg1cl  14262  rrgeq0i  14297  domneq0  14305  2idlelbas  14549  2idlcpblrng  14556  znidomb  14691  toponuni  14758  tpsuni  14777  neipsm  14897  cnf  14947  cnima  14963  txdis1cn  15021  hmeocnvcn  15049  psmetxrge0  15075  isxmet2d  15091  xmstopn  15198  mstopn  15199  bdxmet  15244  divcnap  15308  ivthinclemlr  15380  ivthinclemur  15382  dvlemap  15423  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvrecap  15456  dveflem  15469  plyf  15480  plyadd  15494  plymul  15495  plycn  15505  dvply2g  15509  dvdsppwf1o  15732  mpodvdsmulf1o  15733  lgsfle1  15757  lgsle1  15763  lgsdirprm  15782  lgsne0  15786  lgsquadlem1  15825  lgsquadlem2  15826  upgr1or2  15971  umgredg2en  15979  lfgredg2dom  16002  upgr2wlkdc  16247  trlres  16260  clwwlknon  16299  bj-indsuc  16574  nnsf  16658