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  1777  reurmo  2713  eldifn  3283  elinel2  3347  rabsnt  3694  eldifsni  3748  unimax  3870  ssintub  3889  exmidsssnc  4233  moop2  4281  wepo  4391  wetrep  4392  trssord  4412  ordelord  4413  ordsucim  4533  ordtri2or2exmidlem  4559  regexmidlem1  4566  reg2exmidlema  4567  tfis  4616  opelxp2  4695  funmo  5270  funopg  5289  funco  5295  funun  5299  fununi  5323  funimaexglem  5338  fndm  5354  frn  5413  f1ss  5466  f1ssr  5467  f1ssres  5469  forn  5480  f1f1orn  5512  f1orescnv  5517  f1imacnv  5518  funcocnv2  5526  funfveu  5568  nfvres  5589  isorel  5852  isoini2  5863  f1ofveu  5907  fovcld  6024  f1opw  6127  f1o2ndf1  6283  mpoxopn0yelv  6294  swoer  6617  mapsnconst  6750  en0  6851  en1  6855  phplem4  6913  phplem4dom  6920  phplem4on  6925  ssfilem  6933  diffitest  6945  inffiexmid  6964  supubti  7060  suplubti  7061  djuinr  7124  casefun  7146  casef1  7151  djufun  7165  nnnninfeq  7189  ctssexmid  7211  exmidonfinlem  7255  exmidfodomrlemim  7263  cc4f  7331  cc4n  7333  0npi  7375  mulclpi  7390  mulcanpig  7397  nlt1pig  7403  indpi  7404  nnppipi  7405  dfplpq2  7416  archnqq  7479  enq0tr  7496  nqnq0pi  7500  ltexprlemopl  7663  ltexprlemopu  7665  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemupu  7762  caucvgprprlemdisj  7764  suplocsrlempr  7869  ltresr2  7902  peano2nnnn  7915  axrnegex  7941  ltxrlt  8087  peano2nn  8996  elnn0z  9333  zaddcl  9360  ztri3or0  9362  eluz2gt1  9670  1nuz2  9674  rpgt0  9734  ixxss1  9973  ixxss2  9974  ixxss12  9975  iccss2  10013  iccssico2  10016  elfzuz3  10091  uzdisj  10162  nn0disj  10207  addmodlteq  10472  expge0  10649  expge1  10650  expaddzaplem  10656  shftfn  10971  fsumf1o  11536  fsumge0  11605  fprodf1o  11734  zsupcllemstep  12085  zsupssdc  12094  bezoutlemzz  12142  bezoutlemaz  12143  bezoutlembz  12144  bezoutlemsup  12149  1nprm  12255  nprm  12264  sqnprm  12277  dvdsprm  12278  coprm  12285  sqpweven  12316  2sqpwodd  12317  dfphi2  12361  phimullem  12366  eulerthlemrprm  12370  phisum  12381  expnprm  12494  1arith  12508  4sqlem18  12549  oddennn  12552  znnen  12558  ennnfonelemg  12563  ctinf  12590  mndid  13009  mhmf  13040  mhmlin  13042  mhm0  13043  grpinvex  13085  grplinv  13125  mulgz  13223  mulgdirlem  13226  mulgdir  13227  mulgass  13232  nsgbi  13277  nmzbi  13282  ghmf  13320  ghmlin  13321  conjnsg  13354  ablcmn  13364  cmncom  13375  crngmgp  13503  rhmmhm  13658  rhmghm  13661  rimf1o  13669  nzrnz  13681  subrgss  13721  subrg1cl  13728  rrgeq0i  13763  domneq0  13771  2idlelbas  14015  2idlcpblrng  14022  znidomb  14157  toponuni  14194  tpsuni  14213  neipsm  14333  cnf  14383  cnima  14399  txdis1cn  14457  hmeocnvcn  14485  psmetxrge0  14511  isxmet2d  14527  xmstopn  14634  mstopn  14635  bdxmet  14680  divcnap  14744  ivthinclemlr  14816  ivthinclemur  14818  dvlemap  14859  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvrecap  14892  dveflem  14905  plyf  14916  plyadd  14930  plymul  14931  plycn  14940  lgsfle1  15166  lgsle1  15172  lgsdirprm  15191  lgsne0  15195  lgsquadlem1  15234  lgsquadlem2  15235  bj-indsuc  15490  nnsf  15565