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  948  sb1  1788  reurmo  2724  eldifn  3295  elinel2  3359  rabsnt  3707  eldifsni  3761  unimax  3883  ssintub  3902  exmidsssnc  4246  moop2  4295  wepo  4405  wetrep  4406  trssord  4426  ordelord  4427  ordsucim  4547  ordtri2or2exmidlem  4573  regexmidlem1  4580  reg2exmidlema  4581  tfis  4630  opelxp2  4709  funmo  5285  funopg  5304  funco  5310  funun  5314  fununi  5341  funimaexglem  5356  fndm  5372  frn  5433  f1ss  5486  f1ssr  5487  f1ssres  5489  forn  5500  f1f1orn  5532  f1orescnv  5537  f1imacnv  5538  funcocnv2  5546  funfveu  5588  nfvres  5609  isorel  5876  isoini2  5887  f1ofveu  5931  fovcld  6049  f1opw  6152  f1o2ndf1  6313  mpoxopn0yelv  6324  swoer  6647  mapsnconst  6780  en0  6886  en1  6890  phplem4  6951  phplem4dom  6958  phplem4on  6963  ssfilem  6971  diffitest  6983  inffiexmid  7002  supubti  7100  suplubti  7101  djuinr  7164  casefun  7186  casef1  7191  djufun  7205  nnnninfeq  7229  ctssexmid  7251  exmidonfinlem  7300  exmidfodomrlemim  7308  cc4f  7380  cc4n  7382  0npi  7425  mulclpi  7440  mulcanpig  7447  nlt1pig  7453  indpi  7454  nnppipi  7455  dfplpq2  7466  archnqq  7529  enq0tr  7546  nqnq0pi  7550  ltexprlemopl  7713  ltexprlemopu  7715  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemopu  7760  cauappcvgprlemupu  7761  cauappcvgprlemdisj  7763  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemopu  7783  caucvgprlemupu  7784  caucvgprlemdisj  7786  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemupu  7812  caucvgprprlemdisj  7814  suplocsrlempr  7919  ltresr2  7952  peano2nnnn  7965  axrnegex  7991  ltxrlt  8137  peano2nn  9047  elnn0z  9384  zaddcl  9411  ztri3or0  9413  eluz2gt1  9722  1nuz2  9726  rpgt0  9786  ixxss1  10025  ixxss2  10026  ixxss12  10027  iccss2  10065  iccssico2  10068  elfzuz3  10143  uzdisj  10214  nn0disj  10259  zsupcllemstep  10370  zsupssdc  10379  addmodlteq  10541  expge0  10718  expge1  10719  expaddzaplem  10725  shftfn  11077  fsumf1o  11643  fsumge0  11712  fprodf1o  11841  bitsfzolem  12207  bezoutlemzz  12265  bezoutlemaz  12266  bezoutlembz  12267  bezoutlemsup  12272  1nprm  12378  nprm  12387  sqnprm  12400  dvdsprm  12401  coprm  12408  sqpweven  12439  2sqpwodd  12440  dfphi2  12484  phimullem  12489  eulerthlemrprm  12493  phisum  12505  expnprm  12618  1arith  12632  4sqlem18  12673  oddennn  12705  znnen  12711  ennnfonelemg  12716  ctinf  12743  mndid  13199  mhmf  13239  mhmlin  13241  mhm0  13242  grpinvex  13284  grplinv  13324  mulgz  13428  mulgdirlem  13431  mulgdir  13432  mulgass  13437  nsgbi  13482  nmzbi  13487  ghmf  13525  ghmlin  13526  conjnsg  13559  ablcmn  13569  cmncom  13580  crngmgp  13708  rhmmhm  13863  rhmghm  13866  rimf1o  13874  nzrnz  13886  subrgss  13926  subrg1cl  13933  rrgeq0i  13968  domneq0  13976  2idlelbas  14220  2idlcpblrng  14227  znidomb  14362  toponuni  14429  tpsuni  14448  neipsm  14568  cnf  14618  cnima  14634  txdis1cn  14692  hmeocnvcn  14720  psmetxrge0  14746  isxmet2d  14762  xmstopn  14869  mstopn  14870  bdxmet  14915  divcnap  14979  ivthinclemlr  15051  ivthinclemur  15053  dvlemap  15094  dvcnp2cntop  15113  dvaddxxbr  15115  dvmulxxbr  15116  dvcoapbr  15121  dvcjbr  15122  dvrecap  15127  dveflem  15140  plyf  15151  plyadd  15165  plymul  15166  plycn  15176  dvply2g  15180  dvdsppwf1o  15403  mpodvdsmulf1o  15404  lgsfle1  15428  lgsle1  15434  lgsdirprm  15453  lgsne0  15457  lgsquadlem1  15496  lgsquadlem2  15497  bj-indsuc  15797  nnsf  15875