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  9318  elnn0z  9661  zaddcl  9688  ztri3or0  9690  eluz2gt1  10011  1nuz2  10015  rpgt0  10076  ixxss1  10316  ixxss2  10317  ixxss12  10318  iccss2  10356  iccssico2  10359  elfzuz3  10435  uzdisj  10510  nn0disj  10555  zsupcllemstep  10672  zsupssdc  10683  addmodlteq  10848  expge0  11025  expge1  11026  expaddzaplem  11032  shftfn  11603  fsumf1o  12173  fsumge0  12242  fprodf1o  12371  bitsfzolem  12737  bezoutlemzz  12795  bezoutlemaz  12796  bezoutlembz  12797  bezoutlemsup  12802  1nprm  12908  nprm  12917  sqnprm  12931  dvdsprm  12932  coprm  12939  sqpweven  12971  2sqpwodd  12972  dfphi2  13018  phimullem  13023  eulerthlemrprm  13027  phisum  13039  expnprm  13152  1arith  13166  4sqlem18  13207  ballotfilem4  13290  ballotfilem5  13291  ballotfilemfrc  13319  ballotfilemirc  13324  ballotfilemth  13330  oddennn  13332  znnen  13338  ennnfonelemg  13343  ctinf  13370  mndid  13787  mhmf  13821  mhmlin  13823  mhm0  13824  grpinvex  13864  grplinv  13904  mulgz  14002  mulgdirlem  14005  mulgdir  14006  mulgass  14011  nsgbi  14056  nmzbi  14061  ghmf  14099  ghmlin  14100  conjnsg  14133  ablcmn  14143  cmncom  14154  crngmgp  14357  rhmmhm  14515  rhmghm  14518  rimf1o  14526  nzrnz  14538  subrgss  14579  subrg1cl  14586  rrgeq0i  14621  domneq0  14630  fldcrngd  14665  2idlelbas  14902  2idlcpblrng  14909  znidomb  15042  assalem  15052  toponuni  15165  tpsuni  15184  neipsm  15304  cnf  15354  cnima  15370  txdis1cn  15428  hmeocnvcn  15456  psmetxrge0  15482  isxmet2d  15498  xmstopn  15605  mstopn  15606  bdxmet  15651  divcnap  15715  ivthinclemlr  15787  ivthinclemur  15789  dvlemap  15830  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvrecap  15863  dveflem  15876  plyf  15887  plyadd  15901  plymul  15902  plycn  15912  dvply2g  15916  dvdsppwf1o  16184  mpodvdsmulf1o  16185  lgsfle1  16226  lgsle1  16232  lgsdirprm  16251  lgsne0  16255  lgsquadlem1  16294  lgsquadlem2  16295  upgr1or2  16440  umgredg2en  16448  lfgredg2dom  16471  upgr2wlkdc  16716  trlres  16729  clwwlknon  16768  bj-indsuc  17052  nnsf  17146  als-no-surprise  17245  alseueu  17276