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  1780  reurmo  2716  eldifn  3286  elinel2  3350  rabsnt  3697  eldifsni  3751  unimax  3873  ssintub  3892  exmidsssnc  4236  moop2  4284  wepo  4394  wetrep  4395  trssord  4415  ordelord  4416  ordsucim  4536  ordtri2or2exmidlem  4562  regexmidlem1  4569  reg2exmidlema  4570  tfis  4619  opelxp2  4698  funmo  5273  funopg  5292  funco  5298  funun  5302  fununi  5326  funimaexglem  5341  fndm  5357  frn  5416  f1ss  5469  f1ssr  5470  f1ssres  5472  forn  5483  f1f1orn  5515  f1orescnv  5520  f1imacnv  5521  funcocnv2  5529  funfveu  5571  nfvres  5592  isorel  5855  isoini2  5866  f1ofveu  5910  fovcld  6027  f1opw  6130  f1o2ndf1  6286  mpoxopn0yelv  6297  swoer  6620  mapsnconst  6753  en0  6854  en1  6858  phplem4  6916  phplem4dom  6923  phplem4on  6928  ssfilem  6936  diffitest  6948  inffiexmid  6967  supubti  7065  suplubti  7066  djuinr  7129  casefun  7151  casef1  7156  djufun  7170  nnnninfeq  7194  ctssexmid  7216  exmidonfinlem  7260  exmidfodomrlemim  7268  cc4f  7336  cc4n  7338  0npi  7380  mulclpi  7395  mulcanpig  7402  nlt1pig  7408  indpi  7409  nnppipi  7410  dfplpq2  7421  archnqq  7484  enq0tr  7501  nqnq0pi  7505  ltexprlemopl  7668  ltexprlemopu  7670  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemdisj  7718  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemdisj  7741  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemupu  7767  caucvgprprlemdisj  7769  suplocsrlempr  7874  ltresr2  7907  peano2nnnn  7920  axrnegex  7946  ltxrlt  8092  peano2nn  9002  elnn0z  9339  zaddcl  9366  ztri3or0  9368  eluz2gt1  9676  1nuz2  9680  rpgt0  9740  ixxss1  9979  ixxss2  9980  ixxss12  9981  iccss2  10019  iccssico2  10022  elfzuz3  10097  uzdisj  10168  nn0disj  10213  zsupcllemstep  10319  zsupssdc  10328  addmodlteq  10490  expge0  10667  expge1  10668  expaddzaplem  10674  shftfn  10989  fsumf1o  11555  fsumge0  11624  fprodf1o  11753  bitsfzolem  12118  bezoutlemzz  12169  bezoutlemaz  12170  bezoutlembz  12171  bezoutlemsup  12176  1nprm  12282  nprm  12291  sqnprm  12304  dvdsprm  12305  coprm  12312  sqpweven  12343  2sqpwodd  12344  dfphi2  12388  phimullem  12393  eulerthlemrprm  12397  phisum  12409  expnprm  12522  1arith  12536  4sqlem18  12577  oddennn  12609  znnen  12615  ennnfonelemg  12620  ctinf  12647  mndid  13066  mhmf  13097  mhmlin  13099  mhm0  13100  grpinvex  13142  grplinv  13182  mulgz  13280  mulgdirlem  13283  mulgdir  13284  mulgass  13289  nsgbi  13334  nmzbi  13339  ghmf  13377  ghmlin  13378  conjnsg  13411  ablcmn  13421  cmncom  13432  crngmgp  13560  rhmmhm  13715  rhmghm  13718  rimf1o  13726  nzrnz  13738  subrgss  13778  subrg1cl  13785  rrgeq0i  13820  domneq0  13828  2idlelbas  14072  2idlcpblrng  14079  znidomb  14214  toponuni  14251  tpsuni  14270  neipsm  14390  cnf  14440  cnima  14456  txdis1cn  14514  hmeocnvcn  14542  psmetxrge0  14568  isxmet2d  14584  xmstopn  14691  mstopn  14692  bdxmet  14737  divcnap  14801  ivthinclemlr  14873  ivthinclemur  14875  dvlemap  14916  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvrecap  14949  dveflem  14962  plyf  14973  plyadd  14987  plymul  14988  plycn  14998  dvply2g  15002  dvdsppwf1o  15225  mpodvdsmulf1o  15226  lgsfle1  15250  lgsle1  15256  lgsdirprm  15275  lgsne0  15279  lgsquadlem1  15318  lgsquadlem2  15319  bj-indsuc  15574  nnsf  15649