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  954  sb1  1814  reurmo  2753  eldifn  3330  elinel2  3394  rabsnt  3746  eldifsni  3802  unimax  3927  ssintub  3946  exmidsssnc  4293  moop2  4344  wepo  4456  wetrep  4457  trssord  4477  ordelord  4478  ordsucim  4598  ordtri2or2exmidlem  4624  regexmidlem1  4631  reg2exmidlema  4632  tfis  4681  opelxp2  4760  funmo  5341  funopg  5360  funco  5366  funun  5371  fununi  5398  funimaexglem  5413  fndm  5429  frn  5491  f1ss  5548  f1ssr  5549  f1ssres  5551  forn  5562  f1f1orn  5594  f1orescnv  5599  f1imacnv  5600  funcocnv2  5608  funfveu  5652  nfvres  5675  isorel  5948  isoini2  5959  f1ofveu  6005  fovcld  6125  f1opw  6229  f1o2ndf1  6392  mpoxopn0yelv  6404  swoer  6729  mapsnconst  6862  en0  6968  en1  6972  phplem4  7040  phplem4dom  7047  phplem4on  7053  ssfilem  7061  ssfilemd  7063  diffitest  7075  inffiexmid  7097  supubti  7197  suplubti  7198  djuinr  7261  casefun  7283  casef1  7288  djufun  7302  nnnninfeq  7326  ctssexmid  7348  exmidonfinlem  7403  exmidfodomrlemim  7411  cc4f  7487  cc4n  7489  0npi  7532  mulclpi  7547  mulcanpig  7554  nlt1pig  7560  indpi  7561  nnppipi  7562  dfplpq2  7573  archnqq  7636  enq0tr  7653  nqnq0pi  7657  ltexprlemopl  7820  ltexprlemopu  7822  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemupu  7919  caucvgprprlemdisj  7921  suplocsrlempr  8026  ltresr2  8059  peano2nnnn  8072  axrnegex  8098  ltxrlt  8244  peano2nn  9154  elnn0z  9491  zaddcl  9518  ztri3or0  9520  eluz2gt1  9835  1nuz2  9839  rpgt0  9899  ixxss1  10138  ixxss2  10139  ixxss12  10140  iccss2  10178  iccssico2  10181  elfzuz3  10256  uzdisj  10327  nn0disj  10372  zsupcllemstep  10488  zsupssdc  10497  addmodlteq  10659  expge0  10836  expge1  10837  expaddzaplem  10843  shftfn  11384  fsumf1o  11950  fsumge0  12019  fprodf1o  12148  bitsfzolem  12514  bezoutlemzz  12572  bezoutlemaz  12573  bezoutlembz  12574  bezoutlemsup  12579  1nprm  12685  nprm  12694  sqnprm  12707  dvdsprm  12708  coprm  12715  sqpweven  12746  2sqpwodd  12747  dfphi2  12791  phimullem  12796  eulerthlemrprm  12800  phisum  12812  expnprm  12925  1arith  12939  4sqlem18  12980  oddennn  13012  znnen  13018  ennnfonelemg  13023  ctinf  13050  mndid  13507  mhmf  13547  mhmlin  13549  mhm0  13550  grpinvex  13592  grplinv  13632  mulgz  13736  mulgdirlem  13739  mulgdir  13740  mulgass  13745  nsgbi  13790  nmzbi  13795  ghmf  13833  ghmlin  13834  conjnsg  13867  ablcmn  13877  cmncom  13888  crngmgp  14016  rhmmhm  14172  rhmghm  14175  rimf1o  14183  nzrnz  14195  subrgss  14235  subrg1cl  14242  rrgeq0i  14277  domneq0  14285  2idlelbas  14529  2idlcpblrng  14536  znidomb  14671  toponuni  14738  tpsuni  14757  neipsm  14877  cnf  14927  cnima  14943  txdis1cn  15001  hmeocnvcn  15029  psmetxrge0  15055  isxmet2d  15071  xmstopn  15178  mstopn  15179  bdxmet  15224  divcnap  15288  ivthinclemlr  15360  ivthinclemur  15362  dvlemap  15403  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvrecap  15436  dveflem  15449  plyf  15460  plyadd  15474  plymul  15475  plycn  15485  dvply2g  15489  dvdsppwf1o  15712  mpodvdsmulf1o  15713  lgsfle1  15737  lgsle1  15743  lgsdirprm  15762  lgsne0  15766  lgsquadlem1  15805  lgsquadlem2  15806  upgr1or2  15951  umgredg2en  15959  lfgredg2dom  15982  upgr2wlkdc  16227  trlres  16240  clwwlknon  16279  bj-indsuc  16523  nnsf  16607