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  955  sb1  1815  reurmo  2764  eldifn  3342  elinel2  3406  rabsnt  3766  eldifsni  3822  unimax  3948  ssintub  3967  exmidsssnc  4316  moop2  4368  wepo  4480  wetrep  4481  trssord  4501  ordelord  4502  ordsucim  4622  ordtri2or2exmidlem  4648  regexmidlem1  4655  reg2exmidlema  4656  tfis  4705  opelxp2  4784  funmo  5367  funopg  5386  funco  5392  funun  5397  fununi  5424  funimaexglem  5439  fndm  5455  frn  5517  f1ss  5579  f1ssr  5580  f1ssres  5582  forn  5593  f1f1orn  5625  f1orescnv  5630  f1imacnv  5631  funcocnv2  5639  funfveu  5683  nfvres  5706  isorel  5981  isoini2  5992  f1ofveu  6038  fovcld  6158  f1opw  6262  f1o2ndf1  6424  mpoxopn0yelv  6470  swoer  6795  mapsnconst  6929  en0  7035  en1  7039  phplem4  7109  phplem4dom  7116  phplem4on  7122  ssfilem  7130  ssfilemd  7132  diffitest  7144  inffiexmid  7166  fsuppcorn  7254  supubti  7290  suplubti  7291  djuinr  7354  casefun  7376  casef1  7381  djufun  7395  nnnninfeq  7419  ctssexmid  7441  exmidonfinlem  7496  exmidfodomrlemim  7504  cc4f  7583  cc4n  7585  0npi  7628  mulclpi  7643  mulcanpig  7650  nlt1pig  7656  indpi  7657  nnppipi  7658  dfplpq2  7669  archnqq  7732  enq0tr  7749  nqnq0pi  7753  ltexprlemopl  7916  ltexprlemopu  7918  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemopu  7963  cauappcvgprlemupu  7964  cauappcvgprlemdisj  7966  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemopu  7986  caucvgprlemupu  7987  caucvgprlemdisj  7989  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemupu  8015  caucvgprprlemdisj  8017  suplocsrlempr  8122  ltresr2  8155  peano2nnnn  8168  axrnegex  8194  ltxrlt  8339  peano2nn  9249  elnn0z  9590  zaddcl  9617  ztri3or0  9619  eluz2gt1  9934  1nuz2  9938  rpgt0  9998  ixxss1  10237  ixxss2  10238  ixxss12  10239  iccss2  10277  iccssico2  10280  elfzuz3  10356  uzdisj  10427  nn0disj  10472  zsupcllemstep  10589  zsupssdc  10598  addmodlteq  10760  expge0  10937  expge1  10938  expaddzaplem  10944  shftfn  11509  fsumf1o  12076  fsumge0  12145  fprodf1o  12274  bitsfzolem  12640  bezoutlemzz  12698  bezoutlemaz  12699  bezoutlembz  12700  bezoutlemsup  12705  1nprm  12811  nprm  12820  sqnprm  12833  dvdsprm  12834  coprm  12841  sqpweven  12872  2sqpwodd  12873  dfphi2  12917  phimullem  12922  eulerthlemrprm  12926  phisum  12938  expnprm  13051  1arith  13065  4sqlem18  13106  oddennn  13143  znnen  13149  ennnfonelemg  13154  ctinf  13181  mndid  13638  mhmf  13678  mhmlin  13680  mhm0  13681  grpinvex  13723  grplinv  13763  mulgz  13867  mulgdirlem  13870  mulgdir  13871  mulgass  13876  nsgbi  13921  nmzbi  13926  ghmf  13964  ghmlin  13965  conjnsg  13998  ablcmn  14008  cmncom  14019  crngmgp  14148  rhmmhm  14304  rhmghm  14307  rimf1o  14315  nzrnz  14327  subrgss  14367  subrg1cl  14374  rrgeq0i  14409  domneq0  14418  2idlelbas  14664  2idlcpblrng  14671  znidomb  14806  toponuni  14880  tpsuni  14899  neipsm  15019  cnf  15069  cnima  15085  txdis1cn  15143  hmeocnvcn  15171  psmetxrge0  15197  isxmet2d  15213  xmstopn  15320  mstopn  15321  bdxmet  15366  divcnap  15430  ivthinclemlr  15502  ivthinclemur  15504  dvlemap  15545  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvrecap  15578  dveflem  15591  plyf  15602  plyadd  15616  plymul  15617  plycn  15627  dvply2g  15631  dvdsppwf1o  15857  mpodvdsmulf1o  15858  lgsfle1  15882  lgsle1  15888  lgsdirprm  15907  lgsne0  15911  lgsquadlem1  15950  lgsquadlem2  15951  upgr1or2  16096  umgredg2en  16104  lfgredg2dom  16127  upgr2wlkdc  16372  trlres  16385  clwwlknon  16424  bj-indsuc  16698  nnsf  16783