Theorem simprbi 271

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 119	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simprd 113	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.63dc  911  sb1  1720  reurmo  2617  eldifn  3163  elinel2  3227  rabsnt  3562  eldifsni  3616  unimax  3734  ssintub  3753  exmidsssnc  4084  moop2  4131  wepo  4239  wetrep  4240  trssord  4260  ordelord  4261  ordsucim  4374  ordtri2or2exmidlem  4399  regexmidlem1  4406  reg2exmidlema  4407  tfis  4455  opelxp2  4532  funmo  5094  funopg  5113  funco  5119  funun  5123  fununi  5147  funimaexglem  5162  fndm  5178  frn  5237  f1ss  5290  f1ssr  5291  f1ssres  5293  forn  5304  f1f1orn  5332  f1orescnv  5337  f1imacnv  5338  funcocnv2  5346  funfveu  5386  nfvres  5406  isorel  5661  isoini2  5672  f1ofveu  5714  fovcl  5828  f1opw  5929  f1o2ndf1  6077  mpoxopn0yelv  6088  swoer  6409  mapsnconst  6540  en0  6641  en1  6645  phplem4  6700  phplem4dom  6707  phplem4on  6712  ssfilem  6720  diffitest  6732  inffiexmid  6751  supubti  6836  suplubti  6837  djuinr  6898  casefun  6920  casef1  6925  djufun  6939  ctssexmid  6972  exmidfodomrlemim  7002  0npi  7063  mulclpi  7078  mulcanpig  7085  nlt1pig  7091  indpi  7092  nnppipi  7093  dfplpq2  7104  archnqq  7167  enq0tr  7184  nqnq0pi  7188  ltexprlemopl  7351  ltexprlemopu  7353  cauappcvgprlemopl  7396  cauappcvgprlemlol  7397  cauappcvgprlemopu  7398  cauappcvgprlemupu  7399  cauappcvgprlemdisj  7401  caucvgprlemopl  7419  caucvgprlemlol  7420  caucvgprlemopu  7421  caucvgprlemupu  7422  caucvgprlemdisj  7424  caucvgprprlemopl  7447  caucvgprprlemlol  7448  caucvgprprlemopu  7449  caucvgprprlemupu  7450  caucvgprprlemdisj  7452  ltresr2  7569  peano2nnnn  7582  axrnegex  7608  ltxrlt  7748  peano2nn  8636  elnn0z  8965  zaddcl  8992  ztri3or0  8994  eluz2gt1  9292  1nuz2  9296  rpgt0  9348  ixxss1  9574  ixxss2  9575  ixxss12  9576  iccss2  9614  iccssico2  9617  elfzuz3  9690  uzdisj  9760  nn0disj  9802  addmodlteq  10058  expge0  10216  expge1  10217  expaddzaplem  10223  shftfn  10483  fsumf1o  11045  fsumge0  11114  zsupcllemstep  11480  bezoutlemzz  11530  bezoutlemaz  11531  bezoutlembz  11532  bezoutlemsup  11537  1nprm  11635  nprm  11644  sqnprm  11656  dvdsprm  11657  coprm  11662  sqpweven  11692  2sqpwodd  11693  dfphi2  11735  phimullem  11740  oddennn  11744  znnen  11750  ennnfonelemg  11755  ctinf  11782  toponuni  12019  tpsuni  12038  neipsm  12160  cnf  12209  cnima  12225  txdis1cn  12283  psmetxrge0  12315  isxmet2d  12331  xmstopn  12438  mstopn  12439  bdxmet  12484  divcnap  12535  dvlemap  12598  dvcnp2cntop  12612  dvaddxxbr  12614  bj-indsuc  12809  nnsf  12880  nninfalllemn  12883