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  946  sb1  1766  reurmo  2692  eldifn  3259  elinel2  3323  rabsnt  3668  eldifsni  3722  unimax  3844  ssintub  3863  exmidsssnc  4204  moop2  4252  wepo  4360  wetrep  4361  trssord  4381  ordelord  4382  ordsucim  4500  ordtri2or2exmidlem  4526  regexmidlem1  4533  reg2exmidlema  4534  tfis  4583  opelxp2  4662  funmo  5232  funopg  5251  funco  5257  funun  5261  fununi  5285  funimaexglem  5300  fndm  5316  frn  5375  f1ss  5428  f1ssr  5429  f1ssres  5431  forn  5442  f1f1orn  5473  f1orescnv  5478  f1imacnv  5479  funcocnv2  5487  funfveu  5529  nfvres  5549  isorel  5809  isoini2  5820  f1ofveu  5863  fovcl  5980  f1opw  6078  f1o2ndf1  6229  mpoxopn0yelv  6240  swoer  6563  mapsnconst  6694  en0  6795  en1  6799  phplem4  6855  phplem4dom  6862  phplem4on  6867  ssfilem  6875  diffitest  6887  inffiexmid  6906  supubti  6998  suplubti  6999  djuinr  7062  casefun  7084  casef1  7089  djufun  7103  nnnninfeq  7126  ctssexmid  7148  exmidonfinlem  7192  exmidfodomrlemim  7200  cc4f  7268  cc4n  7270  0npi  7312  mulclpi  7327  mulcanpig  7334  nlt1pig  7340  indpi  7341  nnppipi  7342  dfplpq2  7353  archnqq  7416  enq0tr  7433  nqnq0pi  7437  ltexprlemopl  7600  ltexprlemopu  7602  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemopu  7647  cauappcvgprlemupu  7648  cauappcvgprlemdisj  7650  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemopu  7670  caucvgprlemupu  7671  caucvgprlemdisj  7673  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemupu  7699  caucvgprprlemdisj  7701  suplocsrlempr  7806  ltresr2  7839  peano2nnnn  7852  axrnegex  7878  ltxrlt  8023  peano2nn  8931  elnn0z  9266  zaddcl  9293  ztri3or0  9295  eluz2gt1  9602  1nuz2  9606  rpgt0  9665  ixxss1  9904  ixxss2  9905  ixxss12  9906  iccss2  9944  iccssico2  9947  elfzuz3  10022  uzdisj  10093  nn0disj  10138  addmodlteq  10398  expge0  10556  expge1  10557  expaddzaplem  10563  shftfn  10833  fsumf1o  11398  fsumge0  11467  fprodf1o  11596  zsupcllemstep  11946  zsupssdc  11955  bezoutlemzz  12003  bezoutlemaz  12004  bezoutlembz  12005  bezoutlemsup  12010  1nprm  12114  nprm  12123  sqnprm  12136  dvdsprm  12137  coprm  12144  sqpweven  12175  2sqpwodd  12176  dfphi2  12220  phimullem  12225  eulerthlemrprm  12229  phisum  12240  expnprm  12351  1arith  12365  oddennn  12393  znnen  12399  ennnfonelemg  12404  ctinf  12431  mndid  12826  mhmf  12856  mhmlin  12858  mhm0  12859  grpinvex  12887  grplinv  12922  mulgz  13011  mulgdirlem  13014  mulgdir  13015  mulgass  13020  nsgbi  13064  nmzbi  13069  ablcmn  13095  cmncom  13105  crngmgp  13187  nzrnz  13326  subrgss  13343  subrg1cl  13350  toponuni  13518  tpsuni  13537  neipsm  13657  cnf  13707  cnima  13723  txdis1cn  13781  hmeocnvcn  13809  psmetxrge0  13835  isxmet2d  13851  xmstopn  13958  mstopn  13959  bdxmet  14004  divcnap  14058  ivthinclemlr  14118  ivthinclemur  14120  dvlemap  14152  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  dvrecap  14180  dveflem  14190  lgsfle1  14413  lgsle1  14419  lgsdirprm  14438  lgsne0  14442  bj-indsuc  14683  nnsf  14757