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  948  sb1  1777  reurmo  2713  eldifn  3282  elinel2  3346  rabsnt  3693  eldifsni  3747  unimax  3869  ssintub  3888  exmidsssnc  4232  moop2  4280  wepo  4390  wetrep  4391  trssord  4411  ordelord  4412  ordsucim  4532  ordtri2or2exmidlem  4558  regexmidlem1  4565  reg2exmidlema  4566  tfis  4615  opelxp2  4694  funmo  5269  funopg  5288  funco  5294  funun  5298  fununi  5322  funimaexglem  5337  fndm  5353  frn  5412  f1ss  5465  f1ssr  5466  f1ssres  5468  forn  5479  f1f1orn  5511  f1orescnv  5516  f1imacnv  5517  funcocnv2  5525  funfveu  5567  nfvres  5588  isorel  5851  isoini2  5862  f1ofveu  5906  fovcld  6023  f1opw  6125  f1o2ndf1  6281  mpoxopn0yelv  6292  swoer  6615  mapsnconst  6748  en0  6849  en1  6853  phplem4  6911  phplem4dom  6918  phplem4on  6923  ssfilem  6931  diffitest  6943  inffiexmid  6962  supubti  7058  suplubti  7059  djuinr  7122  casefun  7144  casef1  7149  djufun  7163  nnnninfeq  7187  ctssexmid  7209  exmidonfinlem  7253  exmidfodomrlemim  7261  cc4f  7329  cc4n  7331  0npi  7373  mulclpi  7388  mulcanpig  7395  nlt1pig  7401  indpi  7402  nnppipi  7403  dfplpq2  7414  archnqq  7477  enq0tr  7494  nqnq0pi  7498  ltexprlemopl  7661  ltexprlemopu  7663  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemupu  7760  caucvgprprlemdisj  7762  suplocsrlempr  7867  ltresr2  7900  peano2nnnn  7913  axrnegex  7939  ltxrlt  8085  peano2nn  8994  elnn0z  9330  zaddcl  9357  ztri3or0  9359  eluz2gt1  9667  1nuz2  9671  rpgt0  9731  ixxss1  9970  ixxss2  9971  ixxss12  9972  iccss2  10010  iccssico2  10013  elfzuz3  10088  uzdisj  10159  nn0disj  10204  addmodlteq  10469  expge0  10646  expge1  10647  expaddzaplem  10653  shftfn  10968  fsumf1o  11533  fsumge0  11602  fprodf1o  11731  zsupcllemstep  12082  zsupssdc  12091  bezoutlemzz  12139  bezoutlemaz  12140  bezoutlembz  12141  bezoutlemsup  12146  1nprm  12252  nprm  12261  sqnprm  12274  dvdsprm  12275  coprm  12282  sqpweven  12313  2sqpwodd  12314  dfphi2  12358  phimullem  12363  eulerthlemrprm  12367  phisum  12378  expnprm  12491  1arith  12505  4sqlem18  12546  oddennn  12549  znnen  12555  ennnfonelemg  12560  ctinf  12587  mndid  13006  mhmf  13037  mhmlin  13039  mhm0  13040  grpinvex  13082  grplinv  13122  mulgz  13220  mulgdirlem  13223  mulgdir  13224  mulgass  13229  nsgbi  13274  nmzbi  13279  ghmf  13317  ghmlin  13318  conjnsg  13351  ablcmn  13361  cmncom  13372  crngmgp  13500  rhmmhm  13655  rhmghm  13658  rimf1o  13666  nzrnz  13678  subrgss  13718  subrg1cl  13725  rrgeq0i  13760  domneq0  13768  2idlelbas  14012  2idlcpblrng  14019  znidomb  14146  toponuni  14183  tpsuni  14202  neipsm  14322  cnf  14372  cnima  14388  txdis1cn  14446  hmeocnvcn  14474  psmetxrge0  14500  isxmet2d  14516  xmstopn  14623  mstopn  14624  bdxmet  14669  divcnap  14723  ivthinclemlr  14791  ivthinclemur  14793  dvlemap  14834  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvrecap  14862  dveflem  14872  plyf  14883  plyadd  14897  plymul  14898  lgsfle1  15125  lgsle1  15131  lgsdirprm  15150  lgsne0  15154  lgsquadlem1  15191  bj-indsuc  15420  nnsf  15495