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  955  sb1  1814  reurmo  2754  eldifn  3332  elinel2  3396  rabsnt  3750  eldifsni  3806  unimax  3932  ssintub  3951  exmidsssnc  4299  moop2  4350  wepo  4462  wetrep  4463  trssord  4483  ordelord  4484  ordsucim  4604  ordtri2or2exmidlem  4630  regexmidlem1  4637  reg2exmidlema  4638  tfis  4687  opelxp2  4766  funmo  5348  funopg  5367  funco  5373  funun  5378  fununi  5405  funimaexglem  5420  fndm  5436  frn  5498  f1ss  5557  f1ssr  5558  f1ssres  5560  forn  5571  f1f1orn  5603  f1orescnv  5608  f1imacnv  5609  funcocnv2  5617  funfveu  5661  nfvres  5684  isorel  5959  isoini2  5970  f1ofveu  6016  fovcld  6136  f1opw  6240  f1o2ndf1  6402  mpoxopn0yelv  6448  swoer  6773  mapsnconst  6906  en0  7012  en1  7016  phplem4  7084  phplem4dom  7091  phplem4on  7097  ssfilem  7105  ssfilemd  7107  diffitest  7119  inffiexmid  7141  supubti  7241  suplubti  7242  djuinr  7305  casefun  7327  casef1  7332  djufun  7346  nnnninfeq  7370  ctssexmid  7392  exmidonfinlem  7447  exmidfodomrlemim  7455  cc4f  7531  cc4n  7533  0npi  7576  mulclpi  7591  mulcanpig  7598  nlt1pig  7604  indpi  7605  nnppipi  7606  dfplpq2  7617  archnqq  7680  enq0tr  7697  nqnq0pi  7701  ltexprlemopl  7864  ltexprlemopu  7866  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemdisj  7914  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemdisj  7937  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemupu  7963  caucvgprprlemdisj  7965  suplocsrlempr  8070  ltresr2  8103  peano2nnnn  8116  axrnegex  8142  ltxrlt  8287  peano2nn  9197  elnn0z  9536  zaddcl  9563  ztri3or0  9565  eluz2gt1  9880  1nuz2  9884  rpgt0  9944  ixxss1  10183  ixxss2  10184  ixxss12  10185  iccss2  10223  iccssico2  10226  elfzuz3  10302  uzdisj  10373  nn0disj  10418  zsupcllemstep  10535  zsupssdc  10544  addmodlteq  10706  expge0  10883  expge1  10884  expaddzaplem  10890  shftfn  11447  fsumf1o  12014  fsumge0  12083  fprodf1o  12212  bitsfzolem  12578  bezoutlemzz  12636  bezoutlemaz  12637  bezoutlembz  12638  bezoutlemsup  12643  1nprm  12749  nprm  12758  sqnprm  12771  dvdsprm  12772  coprm  12779  sqpweven  12810  2sqpwodd  12811  dfphi2  12855  phimullem  12860  eulerthlemrprm  12864  phisum  12876  expnprm  12989  1arith  13003  4sqlem18  13044  oddennn  13076  znnen  13082  ennnfonelemg  13087  ctinf  13114  mndid  13571  mhmf  13611  mhmlin  13613  mhm0  13614  grpinvex  13656  grplinv  13696  mulgz  13800  mulgdirlem  13803  mulgdir  13804  mulgass  13809  nsgbi  13854  nmzbi  13859  ghmf  13897  ghmlin  13898  conjnsg  13931  ablcmn  13941  cmncom  13952  crngmgp  14081  rhmmhm  14237  rhmghm  14240  rimf1o  14248  nzrnz  14260  subrgss  14300  subrg1cl  14307  rrgeq0i  14342  domneq0  14351  2idlelbas  14595  2idlcpblrng  14602  znidomb  14737  toponuni  14809  tpsuni  14828  neipsm  14948  cnf  14998  cnima  15014  txdis1cn  15072  hmeocnvcn  15100  psmetxrge0  15126  isxmet2d  15142  xmstopn  15249  mstopn  15250  bdxmet  15295  divcnap  15359  ivthinclemlr  15431  ivthinclemur  15433  dvlemap  15474  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvrecap  15507  dveflem  15520  plyf  15531  plyadd  15545  plymul  15546  plycn  15556  dvply2g  15560  dvdsppwf1o  15786  mpodvdsmulf1o  15787  lgsfle1  15811  lgsle1  15817  lgsdirprm  15836  lgsne0  15840  lgsquadlem1  15879  lgsquadlem2  15880  upgr1or2  16025  umgredg2en  16033  lfgredg2dom  16056  upgr2wlkdc  16301  trlres  16314  clwwlknon  16353  bj-indsuc  16627  nnsf  16714