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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.63dc  959  sb1  1819  reurmo  2772  eldifn  3352  elinel2  3416  rabsnt  3786  eldifsni  3843  unimax  3969  ssintub  3988  exmidsssnc  4342  moop2  4394  wepo  4506  wetrep  4507  trssord  4527  ordelord  4528  ordsucim  4649  ordtri2or2exmidlem  4675  regexmidlem1  4682  reg2exmidlema  4683  tfis  4732  opelxp2  4811  funmo  5395  funopg  5414  funco  5420  funun  5425  fununi  5452  funimaexglem  5467  fndm  5483  frn  5545  f1ss  5607  f1ssr  5608  f1ssres  5610  forn  5621  f1f1orn  5653  f1orescnv  5658  f1imacnv  5659  funcocnv2  5667  funfveu  5711  nfvres  5735  isorel  6017  isoini2  6028  f1ofveu  6076  fovcld  6196  f1opw  6300  f1o2ndf1  6468  mpoxopn0yelv  6515  swoer  6840  mapsnconst  6982  en0  7088  en1  7092  phplem4  7162  phplem4dom  7169  phplem4on  7175  ssfilem  7183  ssfilemd  7185  diffitest  7197  inffiexmid  7219  supubti  7345  suplubti  7346  djuinr  7409  casefun  7431  casef1  7436  djufun  7450  nnnninfeq  7474  ctssexmid  7496  exmidonfinlem  7551  exmidfodomrlemim  7559  cc4f  7641  cc4n  7643  0npi  7686  mulclpi  7701  mulcanpig  7708  nlt1pig  7714  indpi  7715  nnppipi  7716  dfplpq2  7727  archnqq  7790  enq0tr  7807  nqnq0pi  7811  ltexprlemopl  7974  ltexprlemopu  7976  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemupu  8073  caucvgprprlemdisj  8075  suplocsrlempr  8180  ltresr2  8213  peano2nnnn  8226  axrnegex  8252  ltxrlt  8397  peano2nn  9325  elnn0z  9666  zaddcl  9693  ztri3or0  9695  eluz2gt1  10017  1nuz2  10021  rpgt0  10082  ixxss1  10322  ixxss2  10323  ixxss12  10324  iccss2  10362  iccssico2  10365  elfzuz3  10441  uzdisj  10516  nn0disj  10561  zsupcllemstep  10678  zsupssdc  10689  addmodlteq  10855  expge0  11032  expge1  11033  expaddzaplem  11039  shftfn  11610  fsumf1o  12181  fsumge0  12250  fprodf1o  12379  bitsfzolem  12745  bezoutlemzz  12803  bezoutlemaz  12804  bezoutlembz  12805  bezoutlemsup  12810  1nprm  12916  nprm  12925  sqnprm  12939  dvdsprm  12940  coprm  12947  sqpweven  12979  2sqpwodd  12980  dfphi2  13026  phimullem  13031  eulerthlemrprm  13035  phisum  13047  expnprm  13160  1arith  13174  4sqlem18  13215  ballotfilem4  13298  ballotfilem5  13299  ballotfilemfrc  13327  ballotfilemirc  13332  ballotfilemth  13338  oddennn  13340  znnen  13346  ennnfonelemg  13351  ctinf  13378  mndid  13796  mhmf  13830  mhmlin  13832  mhm0  13833  grpinvex  13873  grplinv  13913  mulgz  14011  mulgdirlem  14014  mulgdir  14015  mulgass  14020  nsgbi  14065  nmzbi  14070  ghmf  14108  ghmlin  14109  conjnsg  14142  ablcmn  14183  cmncom  14194  crngmgp  14414  rhmmhm  14574  rhmghm  14577  rimf1o  14585  nzrnz  14597  subrgss  14638  subrg1cl  14645  rrgeq0i  14680  domneq0  14689  fldcrngd  14724  2idlelbas  14961  2idlcpblrng  14968  znidomb  15101  assalem  15111  rhmpsrfilem2  15194  toponuni  15258  tpsuni  15277  neipsm  15397  cnf  15447  cnima  15463  txdis1cn  15521  hmeocnvcn  15549  psmetxrge0  15575  isxmet2d  15591  xmstopn  15698  mstopn  15699  bdxmet  15744  divcnap  15808  ivthinclemlr  15880  ivthinclemur  15882  dvlemap  15923  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvrecap  15956  dveflem  15969  plyf  15980  plyadd  15994  plymul  15995  plycn  16005  dvply2g  16009  efnnfsumcl  16256  efchtqdvds  16282  dvdsppwf1o  16300  mpodvdsmulf1o  16301  lgsfle1  16350  lgsle1  16356  lgsdirprm  16375  lgsne0  16379  lgsquadlem1  16418  lgsquadlem2  16419  upgr1or2  16564  umgredg2en  16572  lfgredg2dom  16595  upgr2wlkdc  16840  trlres  16853  clwwlknon  16892  bj-indsuc  17176  nnsf  17271  als-no-surprise  17371  alseueu  17402