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  7339  suplubti  7340  djuinr  7403  casefun  7425  casef1  7430  djufun  7444  nnnninfeq  7468  ctssexmid  7490  exmidonfinlem  7545  exmidfodomrlemim  7553  cc4f  7635  cc4n  7637  0npi  7680  mulclpi  7695  mulcanpig  7702  nlt1pig  7708  indpi  7709  nnppipi  7710  dfplpq2  7721  archnqq  7784  enq0tr  7801  nqnq0pi  7805  ltexprlemopl  7968  ltexprlemopu  7970  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemupu  8067  caucvgprprlemdisj  8069  suplocsrlempr  8174  ltresr2  8207  peano2nnnn  8220  axrnegex  8246  ltxrlt  8391  peano2nn  9316  elnn0z  9657  zaddcl  9684  ztri3or0  9686  eluz2gt1  10002  1nuz2  10006  rpgt0  10066  ixxss1  10306  ixxss2  10307  ixxss12  10308  iccss2  10346  iccssico2  10349  elfzuz3  10425  uzdisj  10500  nn0disj  10545  zsupcllemstep  10662  zsupssdc  10673  addmodlteq  10835  expge0  11012  expge1  11013  expaddzaplem  11019  shftfn  11589  fsumf1o  12157  fsumge0  12226  fprodf1o  12355  bitsfzolem  12721  bezoutlemzz  12779  bezoutlemaz  12780  bezoutlembz  12781  bezoutlemsup  12786  1nprm  12892  nprm  12901  sqnprm  12914  dvdsprm  12915  coprm  12922  sqpweven  12953  2sqpwodd  12954  dfphi2  12998  phimullem  13003  eulerthlemrprm  13007  phisum  13019  expnprm  13132  1arith  13146  4sqlem18  13187  ballotfilem4  13241  ballotfilem5  13242  ballotfilemfrc  13270  ballotfilemirc  13275  ballotfilemth  13281  oddennn  13283  znnen  13289  ennnfonelemg  13294  ctinf  13321  mndid  13738  mhmf  13772  mhmlin  13774  mhm0  13775  grpinvex  13815  grplinv  13855  mulgz  13953  mulgdirlem  13956  mulgdir  13957  mulgass  13962  nsgbi  14007  nmzbi  14012  ghmf  14050  ghmlin  14051  conjnsg  14084  ablcmn  14094  cmncom  14105  crngmgp  14308  rhmmhm  14466  rhmghm  14469  rimf1o  14477  nzrnz  14489  subrgss  14530  subrg1cl  14537  rrgeq0i  14572  domneq0  14581  fldcrngd  14616  2idlelbas  14853  2idlcpblrng  14860  znidomb  14993  assalem  15003  toponuni  15116  tpsuni  15135  neipsm  15255  cnf  15305  cnima  15321  txdis1cn  15379  hmeocnvcn  15407  psmetxrge0  15433  isxmet2d  15449  xmstopn  15556  mstopn  15557  bdxmet  15602  divcnap  15666  ivthinclemlr  15738  ivthinclemur  15740  dvlemap  15781  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvrecap  15814  dveflem  15827  plyf  15838  plyadd  15852  plymul  15853  plycn  15863  dvply2g  15867  dvdsppwf1o  16103  mpodvdsmulf1o  16104  lgsfle1  16128  lgsle1  16134  lgsdirprm  16153  lgsne0  16157  lgsquadlem1  16196  lgsquadlem2  16197  upgr1or2  16342  umgredg2en  16350  lfgredg2dom  16373  upgr2wlkdc  16618  trlres  16631  clwwlknon  16670  bj-indsuc  16954  nnsf  17048  als-no-surprise  17147  alseueu  17178