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  3287  elinel2  3351  rabsnt  3698  eldifsni  3752  unimax  3874  ssintub  3893  exmidsssnc  4237  moop2  4285  wepo  4395  wetrep  4396  trssord  4416  ordelord  4417  ordsucim  4537  ordtri2or2exmidlem  4563  regexmidlem1  4570  reg2exmidlema  4571  tfis  4620  opelxp2  4699  funmo  5274  funopg  5293  funco  5299  funun  5303  fununi  5327  funimaexglem  5342  fndm  5358  frn  5419  f1ss  5472  f1ssr  5473  f1ssres  5475  forn  5486  f1f1orn  5518  f1orescnv  5523  f1imacnv  5524  funcocnv2  5532  funfveu  5574  nfvres  5595  isorel  5858  isoini2  5869  f1ofveu  5913  fovcld  6031  f1opw  6134  f1o2ndf1  6295  mpoxopn0yelv  6306  swoer  6629  mapsnconst  6762  en0  6863  en1  6867  phplem4  6925  phplem4dom  6932  phplem4on  6937  ssfilem  6945  diffitest  6957  inffiexmid  6976  supubti  7074  suplubti  7075  djuinr  7138  casefun  7160  casef1  7165  djufun  7179  nnnninfeq  7203  ctssexmid  7225  exmidonfinlem  7272  exmidfodomrlemim  7280  cc4f  7352  cc4n  7354  0npi  7397  mulclpi  7412  mulcanpig  7419  nlt1pig  7425  indpi  7426  nnppipi  7427  dfplpq2  7438  archnqq  7501  enq0tr  7518  nqnq0pi  7522  ltexprlemopl  7685  ltexprlemopu  7687  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemdisj  7735  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemdisj  7758  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemupu  7784  caucvgprprlemdisj  7786  suplocsrlempr  7891  ltresr2  7924  peano2nnnn  7937  axrnegex  7963  ltxrlt  8109  peano2nn  9019  elnn0z  9356  zaddcl  9383  ztri3or0  9385  eluz2gt1  9693  1nuz2  9697  rpgt0  9757  ixxss1  9996  ixxss2  9997  ixxss12  9998  iccss2  10036  iccssico2  10039  elfzuz3  10114  uzdisj  10185  nn0disj  10230  zsupcllemstep  10336  zsupssdc  10345  addmodlteq  10507  expge0  10684  expge1  10685  expaddzaplem  10691  shftfn  11006  fsumf1o  11572  fsumge0  11641  fprodf1o  11770  bitsfzolem  12136  bezoutlemzz  12194  bezoutlemaz  12195  bezoutlembz  12196  bezoutlemsup  12201  1nprm  12307  nprm  12316  sqnprm  12329  dvdsprm  12330  coprm  12337  sqpweven  12368  2sqpwodd  12369  dfphi2  12413  phimullem  12418  eulerthlemrprm  12422  phisum  12434  expnprm  12547  1arith  12561  4sqlem18  12602  oddennn  12634  znnen  12640  ennnfonelemg  12645  ctinf  12672  mndid  13127  mhmf  13167  mhmlin  13169  mhm0  13170  grpinvex  13212  grplinv  13252  mulgz  13356  mulgdirlem  13359  mulgdir  13360  mulgass  13365  nsgbi  13410  nmzbi  13415  ghmf  13453  ghmlin  13454  conjnsg  13487  ablcmn  13497  cmncom  13508  crngmgp  13636  rhmmhm  13791  rhmghm  13794  rimf1o  13802  nzrnz  13814  subrgss  13854  subrg1cl  13861  rrgeq0i  13896  domneq0  13904  2idlelbas  14148  2idlcpblrng  14155  znidomb  14290  toponuni  14335  tpsuni  14354  neipsm  14474  cnf  14524  cnima  14540  txdis1cn  14598  hmeocnvcn  14626  psmetxrge0  14652  isxmet2d  14668  xmstopn  14775  mstopn  14776  bdxmet  14821  divcnap  14885  ivthinclemlr  14957  ivthinclemur  14959  dvlemap  15000  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvrecap  15033  dveflem  15046  plyf  15057  plyadd  15071  plymul  15072  plycn  15082  dvply2g  15086  dvdsppwf1o  15309  mpodvdsmulf1o  15310  lgsfle1  15334  lgsle1  15340  lgsdirprm  15359  lgsne0  15363  lgsquadlem1  15402  lgsquadlem2  15403  bj-indsuc  15658  nnsf  15736