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  959  sb1  1819  reurmo  2772  eldifn  3352  elinel2  3416  rabsnt  3782  eldifsni  3838  unimax  3964  ssintub  3983  exmidsssnc  4335  moop2  4387  wepo  4499  wetrep  4500  trssord  4520  ordelord  4521  ordsucim  4642  ordtri2or2exmidlem  4668  regexmidlem1  4675  reg2exmidlema  4676  tfis  4725  opelxp2  4804  funmo  5387  funopg  5406  funco  5412  funun  5417  fununi  5444  funimaexglem  5459  fndm  5475  frn  5537  f1ss  5599  f1ssr  5600  f1ssres  5602  forn  5613  f1f1orn  5645  f1orescnv  5650  f1imacnv  5651  funcocnv2  5659  funfveu  5703  nfvres  5726  isorel  6004  isoini2  6015  f1ofveu  6063  fovcld  6183  f1opw  6287  f1o2ndf1  6454  mpoxopn0yelv  6500  swoer  6825  mapsnconst  6966  en0  7072  en1  7076  phplem4  7146  phplem4dom  7153  phplem4on  7159  ssfilem  7167  ssfilemd  7169  diffitest  7181  inffiexmid  7203  fsuppcorn  7291  supubti  7329  suplubti  7330  djuinr  7393  casefun  7415  casef1  7420  djufun  7434  nnnninfeq  7458  ctssexmid  7480  exmidonfinlem  7535  exmidfodomrlemim  7543  cc4f  7625  cc4n  7627  0npi  7670  mulclpi  7685  mulcanpig  7692  nlt1pig  7698  indpi  7699  nnppipi  7700  dfplpq2  7711  archnqq  7774  enq0tr  7791  nqnq0pi  7795  ltexprlemopl  7958  ltexprlemopu  7960  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemdisj  8008  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemdisj  8031  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemupu  8057  caucvgprprlemdisj  8059  suplocsrlempr  8164  ltresr2  8197  peano2nnnn  8210  axrnegex  8236  ltxrlt  8381  peano2nn  9295  elnn0z  9636  zaddcl  9663  ztri3or0  9665  eluz2gt1  9981  1nuz2  9985  rpgt0  10045  ixxss1  10285  ixxss2  10286  ixxss12  10287  iccss2  10325  iccssico2  10328  elfzuz3  10404  uzdisj  10478  nn0disj  10523  zsupcllemstep  10640  zsupssdc  10651  addmodlteq  10813  expge0  10990  expge1  10991  expaddzaplem  10997  shftfn  11567  fsumf1o  12135  fsumge0  12204  fprodf1o  12333  bitsfzolem  12699  bezoutlemzz  12757  bezoutlemaz  12758  bezoutlembz  12759  bezoutlemsup  12764  1nprm  12870  nprm  12879  sqnprm  12892  dvdsprm  12893  coprm  12900  sqpweven  12931  2sqpwodd  12932  dfphi2  12976  phimullem  12981  eulerthlemrprm  12985  phisum  12997  expnprm  13110  1arith  13124  4sqlem18  13165  ballotfilem4  13219  ballotfilem5  13220  ballotfilemfrc  13248  ballotfilemirc  13253  ballotfilemth  13259  oddennn  13261  znnen  13267  ennnfonelemg  13272  ctinf  13299  mndid  13715  mhmf  13749  mhmlin  13751  mhm0  13752  grpinvex  13792  grplinv  13832  mulgz  13930  mulgdirlem  13933  mulgdir  13934  mulgass  13939  nsgbi  13984  nmzbi  13989  ghmf  14027  ghmlin  14028  conjnsg  14061  ablcmn  14071  cmncom  14082  crngmgp  14282  rhmmhm  14439  rhmghm  14442  rimf1o  14450  nzrnz  14462  subrgss  14503  subrg1cl  14510  rrgeq0i  14545  domneq0  14554  fldcrngd  14589  2idlelbas  14825  2idlcpblrng  14832  znidomb  14965  toponuni  15039  tpsuni  15058  neipsm  15178  cnf  15228  cnima  15244  txdis1cn  15302  hmeocnvcn  15330  psmetxrge0  15356  isxmet2d  15372  xmstopn  15479  mstopn  15480  bdxmet  15525  divcnap  15589  ivthinclemlr  15661  ivthinclemur  15663  dvlemap  15704  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvrecap  15737  dveflem  15750  plyf  15761  plyadd  15775  plymul  15776  plycn  15786  dvply2g  15790  dvdsppwf1o  16017  mpodvdsmulf1o  16018  lgsfle1  16042  lgsle1  16048  lgsdirprm  16067  lgsne0  16071  lgsquadlem1  16110  lgsquadlem2  16111  upgr1or2  16256  umgredg2en  16264  lfgredg2dom  16287  upgr2wlkdc  16532  trlres  16545  clwwlknon  16584  bj-indsuc  16868  nnsf  16953