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  4342  moop2  4394  wepo  4506  wetrep  4507  trssord  4527  ordelord  4528  ordsucim  4649  ordtri2or2exmidlem  4675  regexmidlem1  4682  reg2exmidlema  4683  tfis  4732  opelxp2  4811  funmo  5395  funopg  5414  funco  5420  funun  5425  fununi  5452  funimaexglem  5467  fndm  5483  frn  5545  f1ss  5607  f1ssr  5608  f1ssres  5610  forn  5621  f1f1orn  5653  f1orescnv  5658  f1imacnv  5659  funcocnv2  5667  funfveu  5711  nfvres  5735  isorel  6017  isoini2  6028  f1ofveu  6076  fovcld  6196  f1opw  6300  f1o2ndf1  6468  mpoxopn0yelv  6514  swoer  6839  mapsnconst  6980  en0  7086  en1  7090  phplem4  7160  phplem4dom  7167  phplem4on  7173  ssfilem  7181  ssfilemd  7183  diffitest  7195  inffiexmid  7217  fsuppcorn  7306  supubti  7345  suplubti  7346  djuinr  7409  casefun  7431  casef1  7436  djufun  7450  nnnninfeq  7474  ctssexmid  7496  exmidonfinlem  7551  exmidfodomrlemim  7559  cc4f  7641  cc4n  7643  0npi  7686  mulclpi  7701  mulcanpig  7708  nlt1pig  7714  indpi  7715  nnppipi  7716  dfplpq2  7727  archnqq  7790  enq0tr  7807  nqnq0pi  7811  ltexprlemopl  7974  ltexprlemopu  7976  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemupu  8073  caucvgprprlemdisj  8075  suplocsrlempr  8180  ltresr2  8213  peano2nnnn  8226  axrnegex  8252  ltxrlt  8397  peano2nn  9325  elnn0z  9668  zaddcl  9695  ztri3or0  9697  eluz2gt1  10018  1nuz2  10022  rpgt0  10083  ixxss1  10323  ixxss2  10324  ixxss12  10325  iccss2  10363  iccssico2  10366  elfzuz3  10442  uzdisj  10517  nn0disj  10562  zsupcllemstep  10679  zsupssdc  10690  addmodlteq  10856  expge0  11033  expge1  11034  expaddzaplem  11040  shftfn  11611  fsumf1o  12182  fsumge0  12251  fprodf1o  12380  bitsfzolem  12746  bezoutlemzz  12804  bezoutlemaz  12805  bezoutlembz  12806  bezoutlemsup  12811  1nprm  12917  nprm  12926  sqnprm  12940  dvdsprm  12941  coprm  12948  sqpweven  12980  2sqpwodd  12981  dfphi2  13027  phimullem  13032  eulerthlemrprm  13036  phisum  13048  expnprm  13161  1arith  13175  4sqlem18  13216  ballotfilem4  13299  ballotfilem5  13300  ballotfilemfrc  13328  ballotfilemirc  13333  ballotfilemth  13339  oddennn  13341  znnen  13347  ennnfonelemg  13352  ctinf  13379  mndid  13797  mhmf  13831  mhmlin  13833  mhm0  13834  grpinvex  13874  grplinv  13914  mulgz  14012  mulgdirlem  14015  mulgdir  14016  mulgass  14021  nsgbi  14066  nmzbi  14071  ghmf  14109  ghmlin  14110  conjnsg  14143  ablcmn  14184  cmncom  14195  crngmgp  14415  rhmmhm  14575  rhmghm  14578  rimf1o  14586  nzrnz  14598  subrgss  14639  subrg1cl  14646  rrgeq0i  14681  domneq0  14690  fldcrngd  14725  2idlelbas  14962  2idlcpblrng  14969  znidomb  15102  assalem  15112  rhmpsrfilem2  15185  toponuni  15241  tpsuni  15260  neipsm  15380  cnf  15430  cnima  15446  txdis1cn  15504  hmeocnvcn  15532  psmetxrge0  15558  isxmet2d  15574  xmstopn  15681  mstopn  15682  bdxmet  15727  divcnap  15791  ivthinclemlr  15863  ivthinclemur  15865  dvlemap  15906  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvrecap  15939  dveflem  15952  plyf  15963  plyadd  15977  plymul  15978  plycn  15988  dvply2g  15992  efnnfsumcl  16239  efchtqdvds  16265  dvdsppwf1o  16283  mpodvdsmulf1o  16284  lgsfle1  16333  lgsle1  16339  lgsdirprm  16358  lgsne0  16362  lgsquadlem1  16401  lgsquadlem2  16402  upgr1or2  16547  umgredg2en  16555  lfgredg2dom  16578  upgr2wlkdc  16823  trlres  16836  clwwlknon  16875  bj-indsuc  17159  nnsf  17254  als-no-surprise  17354  alseueu  17385