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  949  sb1  1790  reurmo  2726  eldifn  3300  elinel2  3364  rabsnt  3713  eldifsni  3768  unimax  3890  ssintub  3909  exmidsssnc  4255  moop2  4304  wepo  4414  wetrep  4415  trssord  4435  ordelord  4436  ordsucim  4556  ordtri2or2exmidlem  4582  regexmidlem1  4589  reg2exmidlema  4590  tfis  4639  opelxp2  4718  funmo  5295  funopg  5314  funco  5320  funun  5324  fununi  5351  funimaexglem  5366  fndm  5382  frn  5444  f1ss  5499  f1ssr  5500  f1ssres  5502  forn  5513  f1f1orn  5545  f1orescnv  5550  f1imacnv  5551  funcocnv2  5559  funfveu  5602  nfvres  5623  isorel  5890  isoini2  5901  f1ofveu  5945  fovcld  6063  f1opw  6166  f1o2ndf1  6327  mpoxopn0yelv  6338  swoer  6661  mapsnconst  6794  en0  6900  en1  6904  phplem4  6967  phplem4dom  6974  phplem4on  6979  ssfilem  6987  diffitest  6999  inffiexmid  7018  supubti  7116  suplubti  7117  djuinr  7180  casefun  7202  casef1  7207  djufun  7221  nnnninfeq  7245  ctssexmid  7267  exmidonfinlem  7317  exmidfodomrlemim  7325  cc4f  7401  cc4n  7403  0npi  7446  mulclpi  7461  mulcanpig  7468  nlt1pig  7474  indpi  7475  nnppipi  7476  dfplpq2  7487  archnqq  7550  enq0tr  7567  nqnq0pi  7571  ltexprlemopl  7734  ltexprlemopu  7736  cauappcvgprlemopl  7779  cauappcvgprlemlol  7780  cauappcvgprlemopu  7781  cauappcvgprlemupu  7782  cauappcvgprlemdisj  7784  caucvgprlemopl  7802  caucvgprlemlol  7803  caucvgprlemopu  7804  caucvgprlemupu  7805  caucvgprlemdisj  7807  caucvgprprlemopl  7830  caucvgprprlemlol  7831  caucvgprprlemopu  7832  caucvgprprlemupu  7833  caucvgprprlemdisj  7835  suplocsrlempr  7940  ltresr2  7973  peano2nnnn  7986  axrnegex  8012  ltxrlt  8158  peano2nn  9068  elnn0z  9405  zaddcl  9432  ztri3or0  9434  eluz2gt1  9743  1nuz2  9747  rpgt0  9807  ixxss1  10046  ixxss2  10047  ixxss12  10048  iccss2  10086  iccssico2  10089  elfzuz3  10164  uzdisj  10235  nn0disj  10280  zsupcllemstep  10394  zsupssdc  10403  addmodlteq  10565  expge0  10742  expge1  10743  expaddzaplem  10749  shftfn  11210  fsumf1o  11776  fsumge0  11845  fprodf1o  11974  bitsfzolem  12340  bezoutlemzz  12398  bezoutlemaz  12399  bezoutlembz  12400  bezoutlemsup  12405  1nprm  12511  nprm  12520  sqnprm  12533  dvdsprm  12534  coprm  12541  sqpweven  12572  2sqpwodd  12573  dfphi2  12617  phimullem  12622  eulerthlemrprm  12626  phisum  12638  expnprm  12751  1arith  12765  4sqlem18  12806  oddennn  12838  znnen  12844  ennnfonelemg  12849  ctinf  12876  mndid  13332  mhmf  13372  mhmlin  13374  mhm0  13375  grpinvex  13417  grplinv  13457  mulgz  13561  mulgdirlem  13564  mulgdir  13565  mulgass  13570  nsgbi  13615  nmzbi  13620  ghmf  13658  ghmlin  13659  conjnsg  13692  ablcmn  13702  cmncom  13713  crngmgp  13841  rhmmhm  13996  rhmghm  13999  rimf1o  14007  nzrnz  14019  subrgss  14059  subrg1cl  14066  rrgeq0i  14101  domneq0  14109  2idlelbas  14353  2idlcpblrng  14360  znidomb  14495  toponuni  14562  tpsuni  14581  neipsm  14701  cnf  14751  cnima  14767  txdis1cn  14825  hmeocnvcn  14853  psmetxrge0  14879  isxmet2d  14895  xmstopn  15002  mstopn  15003  bdxmet  15048  divcnap  15112  ivthinclemlr  15184  ivthinclemur  15186  dvlemap  15227  dvcnp2cntop  15246  dvaddxxbr  15248  dvmulxxbr  15249  dvcoapbr  15254  dvcjbr  15255  dvrecap  15260  dveflem  15273  plyf  15284  plyadd  15298  plymul  15299  plycn  15309  dvply2g  15313  dvdsppwf1o  15536  mpodvdsmulf1o  15537  lgsfle1  15561  lgsle1  15567  lgsdirprm  15586  lgsne0  15590  lgsquadlem1  15629  lgsquadlem2  15630  upgr1or2  15772  umgredg2en  15780  bj-indsuc  16002  nnsf  16083