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  3328  elinel2  3392  rabsnt  3744  eldifsni  3800  unimax  3925  ssintub  3944  exmidsssnc  4291  moop2  4342  wepo  4454  wetrep  4455  trssord  4475  ordelord  4476  ordsucim  4596  ordtri2or2exmidlem  4622  regexmidlem1  4629  reg2exmidlema  4630  tfis  4679  opelxp2  4758  funmo  5339  funopg  5358  funco  5364  funun  5368  fununi  5395  funimaexglem  5410  fndm  5426  frn  5488  f1ss  5545  f1ssr  5546  f1ssres  5548  forn  5559  f1f1orn  5591  f1orescnv  5596  f1imacnv  5597  funcocnv2  5605  funfveu  5648  nfvres  5671  isorel  5944  isoini2  5955  f1ofveu  6001  fovcld  6121  f1opw  6225  f1o2ndf1  6388  mpoxopn0yelv  6400  swoer  6725  mapsnconst  6858  en0  6964  en1  6968  phplem4  7036  phplem4dom  7043  phplem4on  7049  ssfilem  7057  diffitest  7069  inffiexmid  7091  supubti  7189  suplubti  7190  djuinr  7253  casefun  7275  casef1  7280  djufun  7294  nnnninfeq  7318  ctssexmid  7340  exmidonfinlem  7394  exmidfodomrlemim  7402  cc4f  7478  cc4n  7480  0npi  7523  mulclpi  7538  mulcanpig  7545  nlt1pig  7551  indpi  7552  nnppipi  7553  dfplpq2  7564  archnqq  7627  enq0tr  7644  nqnq0pi  7648  ltexprlemopl  7811  ltexprlemopu  7813  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemdisj  7861  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemdisj  7884  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemupu  7910  caucvgprprlemdisj  7912  suplocsrlempr  8017  ltresr2  8050  peano2nnnn  8063  axrnegex  8089  ltxrlt  8235  peano2nn  9145  elnn0z  9482  zaddcl  9509  ztri3or0  9511  eluz2gt1  9826  1nuz2  9830  rpgt0  9890  ixxss1  10129  ixxss2  10130  ixxss12  10131  iccss2  10169  iccssico2  10172  elfzuz3  10247  uzdisj  10318  nn0disj  10363  zsupcllemstep  10479  zsupssdc  10488  addmodlteq  10650  expge0  10827  expge1  10828  expaddzaplem  10834  shftfn  11375  fsumf1o  11941  fsumge0  12010  fprodf1o  12139  bitsfzolem  12505  bezoutlemzz  12563  bezoutlemaz  12564  bezoutlembz  12565  bezoutlemsup  12570  1nprm  12676  nprm  12685  sqnprm  12698  dvdsprm  12699  coprm  12706  sqpweven  12737  2sqpwodd  12738  dfphi2  12782  phimullem  12787  eulerthlemrprm  12791  phisum  12803  expnprm  12916  1arith  12930  4sqlem18  12971  oddennn  13003  znnen  13009  ennnfonelemg  13014  ctinf  13041  mndid  13498  mhmf  13538  mhmlin  13540  mhm0  13541  grpinvex  13583  grplinv  13623  mulgz  13727  mulgdirlem  13730  mulgdir  13731  mulgass  13736  nsgbi  13781  nmzbi  13786  ghmf  13824  ghmlin  13825  conjnsg  13858  ablcmn  13868  cmncom  13879  crngmgp  14007  rhmmhm  14163  rhmghm  14166  rimf1o  14174  nzrnz  14186  subrgss  14226  subrg1cl  14233  rrgeq0i  14268  domneq0  14276  2idlelbas  14520  2idlcpblrng  14527  znidomb  14662  toponuni  14729  tpsuni  14748  neipsm  14868  cnf  14918  cnima  14934  txdis1cn  14992  hmeocnvcn  15020  psmetxrge0  15046  isxmet2d  15062  xmstopn  15169  mstopn  15170  bdxmet  15215  divcnap  15279  ivthinclemlr  15351  ivthinclemur  15353  dvlemap  15394  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvrecap  15427  dveflem  15440  plyf  15451  plyadd  15465  plymul  15466  plycn  15476  dvply2g  15480  dvdsppwf1o  15703  mpodvdsmulf1o  15704  lgsfle1  15728  lgsle1  15734  lgsdirprm  15753  lgsne0  15757  lgsquadlem1  15796  lgsquadlem2  15797  upgr1or2  15942  umgredg2en  15950  lfgredg2dom  15971  upgr2wlkdc  16172  trlres  16185  clwwlknon  16224  bj-indsuc  16459  nnsf  16543