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  4340  moop2  4392  wepo  4504  wetrep  4505  trssord  4525  ordelord  4526  ordsucim  4647  ordtri2or2exmidlem  4673  regexmidlem1  4680  reg2exmidlema  4681  tfis  4730  opelxp2  4809  funmo  5392  funopg  5411  funco  5417  funun  5422  fununi  5449  funimaexglem  5464  fndm  5480  frn  5542  f1ss  5604  f1ssr  5605  f1ssres  5607  forn  5618  f1f1orn  5650  f1orescnv  5655  f1imacnv  5656  funcocnv2  5664  funfveu  5708  nfvres  5732  isorel  6014  isoini2  6025  f1ofveu  6073  fovcld  6193  f1opw  6297  f1o2ndf1  6464  mpoxopn0yelv  6510  swoer  6835  mapsnconst  6976  en0  7082  en1  7086  phplem4  7156  phplem4dom  7163  phplem4on  7169  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  fsuppcorn  7301  supubti  7340  suplubti  7341  djuinr  7404  casefun  7426  casef1  7431  djufun  7445  nnnninfeq  7469  ctssexmid  7491  exmidonfinlem  7546  exmidfodomrlemim  7554  cc4f  7636  cc4n  7638  0npi  7681  mulclpi  7696  mulcanpig  7703  nlt1pig  7709  indpi  7710  nnppipi  7711  dfplpq2  7722  archnqq  7785  enq0tr  7802  nqnq0pi  7806  ltexprlemopl  7969  ltexprlemopu  7971  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemupu  8068  caucvgprprlemdisj  8070  suplocsrlempr  8175  ltresr2  8208  peano2nnnn  8221  axrnegex  8247  ltxrlt  8392  peano2nn  9319  elnn0z  9662  zaddcl  9689  ztri3or0  9691  eluz2gt1  10012  1nuz2  10016  rpgt0  10077  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iccssico2  10360  elfzuz3  10436  uzdisj  10511  nn0disj  10556  zsupcllemstep  10673  zsupssdc  10684  addmodlteq  10850  expge0  11027  expge1  11028  expaddzaplem  11034  shftfn  11605  fsumf1o  12176  fsumge0  12245  fprodf1o  12374  bitsfzolem  12740  bezoutlemzz  12798  bezoutlemaz  12799  bezoutlembz  12800  bezoutlemsup  12805  1nprm  12911  nprm  12920  sqnprm  12934  dvdsprm  12935  coprm  12942  sqpweven  12974  2sqpwodd  12975  dfphi2  13021  phimullem  13026  eulerthlemrprm  13030  phisum  13042  expnprm  13155  1arith  13169  4sqlem18  13210  ballotfilem4  13293  ballotfilem5  13294  ballotfilemfrc  13322  ballotfilemirc  13327  ballotfilemth  13333  oddennn  13335  znnen  13341  ennnfonelemg  13346  ctinf  13373  mndid  13791  mhmf  13825  mhmlin  13827  mhm0  13828  grpinvex  13868  grplinv  13908  mulgz  14006  mulgdirlem  14009  mulgdir  14010  mulgass  14015  nsgbi  14060  nmzbi  14065  ghmf  14103  ghmlin  14104  conjnsg  14137  ablcmn  14178  cmncom  14189  crngmgp  14392  rhmmhm  14550  rhmghm  14553  rimf1o  14561  nzrnz  14573  subrgss  14614  subrg1cl  14621  rrgeq0i  14656  domneq0  14665  fldcrngd  14700  2idlelbas  14937  2idlcpblrng  14944  znidomb  15077  assalem  15087  rhmpsrfilem2  15157  toponuni  15207  tpsuni  15226  neipsm  15346  cnf  15396  cnima  15412  txdis1cn  15470  hmeocnvcn  15498  psmetxrge0  15524  isxmet2d  15540  xmstopn  15647  mstopn  15648  bdxmet  15693  divcnap  15757  ivthinclemlr  15829  ivthinclemur  15831  dvlemap  15872  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvrecap  15905  dveflem  15918  plyf  15929  plyadd  15943  plymul  15944  plycn  15954  dvply2g  15958  efnnfsumcl  16200  efchtqdvds  16226  dvdsppwf1o  16244  mpodvdsmulf1o  16245  lgsfle1  16294  lgsle1  16300  lgsdirprm  16319  lgsne0  16323  lgsquadlem1  16362  lgsquadlem2  16363  upgr1or2  16508  umgredg2en  16516  lfgredg2dom  16539  upgr2wlkdc  16784  trlres  16797  clwwlknon  16836  bj-indsuc  17120  nnsf  17214  als-no-surprise  17314  alseueu  17345