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  952  sb1  1812  reurmo  2751  eldifn  3327  elinel2  3391  rabsnt  3741  eldifsni  3796  unimax  3921  ssintub  3940  exmidsssnc  4286  moop2  4337  wepo  4449  wetrep  4450  trssord  4470  ordelord  4471  ordsucim  4591  ordtri2or2exmidlem  4617  regexmidlem1  4624  reg2exmidlema  4625  tfis  4674  opelxp2  4753  funmo  5332  funopg  5351  funco  5357  funun  5361  fununi  5388  funimaexglem  5403  fndm  5419  frn  5481  f1ss  5536  f1ssr  5537  f1ssres  5539  forn  5550  f1f1orn  5582  f1orescnv  5587  f1imacnv  5588  funcocnv2  5596  funfveu  5639  nfvres  5662  isorel  5931  isoini2  5942  f1ofveu  5988  fovcld  6108  f1opw  6211  f1o2ndf1  6372  mpoxopn0yelv  6383  swoer  6706  mapsnconst  6839  en0  6945  en1  6949  phplem4  7012  phplem4dom  7019  phplem4on  7025  ssfilem  7033  diffitest  7045  inffiexmid  7064  supubti  7162  suplubti  7163  djuinr  7226  casefun  7248  casef1  7253  djufun  7267  nnnninfeq  7291  ctssexmid  7313  exmidonfinlem  7367  exmidfodomrlemim  7375  cc4f  7451  cc4n  7453  0npi  7496  mulclpi  7511  mulcanpig  7518  nlt1pig  7524  indpi  7525  nnppipi  7526  dfplpq2  7537  archnqq  7600  enq0tr  7617  nqnq0pi  7621  ltexprlemopl  7784  ltexprlemopu  7786  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemopu  7831  cauappcvgprlemupu  7832  cauappcvgprlemdisj  7834  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemopu  7854  caucvgprlemupu  7855  caucvgprlemdisj  7857  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemupu  7883  caucvgprprlemdisj  7885  suplocsrlempr  7990  ltresr2  8023  peano2nnnn  8036  axrnegex  8062  ltxrlt  8208  peano2nn  9118  elnn0z  9455  zaddcl  9482  ztri3or0  9484  eluz2gt1  9793  1nuz2  9797  rpgt0  9857  ixxss1  10096  ixxss2  10097  ixxss12  10098  iccss2  10136  iccssico2  10139  elfzuz3  10214  uzdisj  10285  nn0disj  10330  zsupcllemstep  10444  zsupssdc  10453  addmodlteq  10615  expge0  10792  expge1  10793  expaddzaplem  10799  shftfn  11330  fsumf1o  11896  fsumge0  11965  fprodf1o  12094  bitsfzolem  12460  bezoutlemzz  12518  bezoutlemaz  12519  bezoutlembz  12520  bezoutlemsup  12525  1nprm  12631  nprm  12640  sqnprm  12653  dvdsprm  12654  coprm  12661  sqpweven  12692  2sqpwodd  12693  dfphi2  12737  phimullem  12742  eulerthlemrprm  12746  phisum  12758  expnprm  12871  1arith  12885  4sqlem18  12926  oddennn  12958  znnen  12964  ennnfonelemg  12969  ctinf  12996  mndid  13453  mhmf  13493  mhmlin  13495  mhm0  13496  grpinvex  13538  grplinv  13578  mulgz  13682  mulgdirlem  13685  mulgdir  13686  mulgass  13691  nsgbi  13736  nmzbi  13741  ghmf  13779  ghmlin  13780  conjnsg  13813  ablcmn  13823  cmncom  13834  crngmgp  13962  rhmmhm  14117  rhmghm  14120  rimf1o  14128  nzrnz  14140  subrgss  14180  subrg1cl  14187  rrgeq0i  14222  domneq0  14230  2idlelbas  14474  2idlcpblrng  14481  znidomb  14616  toponuni  14683  tpsuni  14702  neipsm  14822  cnf  14872  cnima  14888  txdis1cn  14946  hmeocnvcn  14974  psmetxrge0  15000  isxmet2d  15016  xmstopn  15123  mstopn  15124  bdxmet  15169  divcnap  15233  ivthinclemlr  15305  ivthinclemur  15307  dvlemap  15348  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  dvrecap  15381  dveflem  15394  plyf  15405  plyadd  15419  plymul  15420  plycn  15430  dvply2g  15434  dvdsppwf1o  15657  mpodvdsmulf1o  15658  lgsfle1  15682  lgsle1  15688  lgsdirprm  15707  lgsne0  15711  lgsquadlem1  15750  lgsquadlem2  15751  upgr1or2  15895  umgredg2en  15903  lfgredg2dom  15924  bj-indsuc  16249  nnsf  16330