Theorem simprbi 273

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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.63dc  935  sb1  1753  reurmo  2678  eldifn  3240  elinel2  3304  rabsnt  3645  eldifsni  3699  unimax  3817  ssintub  3836  exmidsssnc  4176  moop2  4223  wepo  4331  wetrep  4332  trssord  4352  ordelord  4353  ordsucim  4471  ordtri2or2exmidlem  4497  regexmidlem1  4504  reg2exmidlema  4505  tfis  4554  opelxp2  4633  funmo  5197  funopg  5216  funco  5222  funun  5226  fununi  5250  funimaexglem  5265  fndm  5281  frn  5340  f1ss  5393  f1ssr  5394  f1ssres  5396  forn  5407  f1f1orn  5437  f1orescnv  5442  f1imacnv  5443  funcocnv2  5451  funfveu  5493  nfvres  5513  isorel  5770  isoini2  5781  f1ofveu  5824  fovcl  5938  f1opw  6039  f1o2ndf1  6187  mpoxopn0yelv  6198  swoer  6520  mapsnconst  6651  en0  6752  en1  6756  phplem4  6812  phplem4dom  6819  phplem4on  6824  ssfilem  6832  diffitest  6844  inffiexmid  6863  supubti  6955  suplubti  6956  djuinr  7019  casefun  7041  casef1  7046  djufun  7060  nnnninfeq  7083  ctssexmid  7105  exmidonfinlem  7140  exmidfodomrlemim  7148  cc4f  7201  cc4n  7203  0npi  7245  mulclpi  7260  mulcanpig  7267  nlt1pig  7273  indpi  7274  nnppipi  7275  dfplpq2  7286  archnqq  7349  enq0tr  7366  nqnq0pi  7370  ltexprlemopl  7533  ltexprlemopu  7535  cauappcvgprlemopl  7578  cauappcvgprlemlol  7579  cauappcvgprlemopu  7580  cauappcvgprlemupu  7581  cauappcvgprlemdisj  7583  caucvgprlemopl  7601  caucvgprlemlol  7602  caucvgprlemopu  7603  caucvgprlemupu  7604  caucvgprlemdisj  7606  caucvgprprlemopl  7629  caucvgprprlemlol  7630  caucvgprprlemopu  7631  caucvgprprlemupu  7632  caucvgprprlemdisj  7634  suplocsrlempr  7739  ltresr2  7772  peano2nnnn  7785  axrnegex  7811  ltxrlt  7955  peano2nn  8860  elnn0z  9195  zaddcl  9222  ztri3or0  9224  eluz2gt1  9531  1nuz2  9535  rpgt0  9592  ixxss1  9831  ixxss2  9832  ixxss12  9833  iccss2  9871  iccssico2  9874  elfzuz3  9948  uzdisj  10018  nn0disj  10063  addmodlteq  10323  expge0  10481  expge1  10482  expaddzaplem  10488  shftfn  10752  fsumf1o  11317  fsumge0  11386  fprodf1o  11515  zsupcllemstep  11863  zsupssdc  11872  bezoutlemzz  11920  bezoutlemaz  11921  bezoutlembz  11922  bezoutlemsup  11927  1nprm  12025  nprm  12034  sqnprm  12047  dvdsprm  12048  coprm  12053  sqpweven  12084  2sqpwodd  12085  dfphi2  12129  phimullem  12134  eulerthlemrprm  12138  phisum  12149  expnprm  12260  oddennn  12262  znnen  12268  ennnfonelemg  12273  ctinf  12300  toponuni  12554  tpsuni  12573  neipsm  12695  cnf  12745  cnima  12761  txdis1cn  12819  hmeocnvcn  12847  psmetxrge0  12873  isxmet2d  12889  xmstopn  12996  mstopn  12997  bdxmet  13042  divcnap  13096  ivthinclemlr  13156  ivthinclemur  13158  dvlemap  13190  dvcnp2cntop  13204  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvcjbr  13213  dvrecap  13218  dveflem  13228  bj-indsuc  13645  nnsf  13719