Theorem simprbi 273

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 119	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simprd 113	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.63dc  941  sb1  1759  reurmo  2684  eldifn  3250  elinel2  3314  rabsnt  3658  eldifsni  3712  unimax  3830  ssintub  3849  exmidsssnc  4189  moop2  4236  wepo  4344  wetrep  4345  trssord  4365  ordelord  4366  ordsucim  4484  ordtri2or2exmidlem  4510  regexmidlem1  4517  reg2exmidlema  4518  tfis  4567  opelxp2  4646  funmo  5213  funopg  5232  funco  5238  funun  5242  fununi  5266  funimaexglem  5281  fndm  5297  frn  5356  f1ss  5409  f1ssr  5410  f1ssres  5412  forn  5423  f1f1orn  5453  f1orescnv  5458  f1imacnv  5459  funcocnv2  5467  funfveu  5509  nfvres  5529  isorel  5787  isoini2  5798  f1ofveu  5841  fovcl  5958  f1opw  6056  f1o2ndf1  6207  mpoxopn0yelv  6218  swoer  6541  mapsnconst  6672  en0  6773  en1  6777  phplem4  6833  phplem4dom  6840  phplem4on  6845  ssfilem  6853  diffitest  6865  inffiexmid  6884  supubti  6976  suplubti  6977  djuinr  7040  casefun  7062  casef1  7067  djufun  7081  nnnninfeq  7104  ctssexmid  7126  exmidonfinlem  7170  exmidfodomrlemim  7178  cc4f  7231  cc4n  7233  0npi  7275  mulclpi  7290  mulcanpig  7297  nlt1pig  7303  indpi  7304  nnppipi  7305  dfplpq2  7316  archnqq  7379  enq0tr  7396  nqnq0pi  7400  ltexprlemopl  7563  ltexprlemopu  7565  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemupu  7662  caucvgprprlemdisj  7664  suplocsrlempr  7769  ltresr2  7802  peano2nnnn  7815  axrnegex  7841  ltxrlt  7985  peano2nn  8890  elnn0z  9225  zaddcl  9252  ztri3or0  9254  eluz2gt1  9561  1nuz2  9565  rpgt0  9622  ixxss1  9861  ixxss2  9862  ixxss12  9863  iccss2  9901  iccssico2  9904  elfzuz3  9978  uzdisj  10049  nn0disj  10094  addmodlteq  10354  expge0  10512  expge1  10513  expaddzaplem  10519  shftfn  10788  fsumf1o  11353  fsumge0  11422  fprodf1o  11551  zsupcllemstep  11900  zsupssdc  11909  bezoutlemzz  11957  bezoutlemaz  11958  bezoutlembz  11959  bezoutlemsup  11964  1nprm  12068  nprm  12077  sqnprm  12090  dvdsprm  12091  coprm  12098  sqpweven  12129  2sqpwodd  12130  dfphi2  12174  phimullem  12179  eulerthlemrprm  12183  phisum  12194  expnprm  12305  1arith  12319  oddennn  12347  znnen  12353  ennnfonelemg  12358  ctinf  12385  mndid  12661  mhmf  12688  mhmlin  12690  mhm0  12691  grpinvex  12718  grplinv  12752  toponuni  12807  tpsuni  12826  neipsm  12948  cnf  12998  cnima  13014  txdis1cn  13072  hmeocnvcn  13100  psmetxrge0  13126  isxmet2d  13142  xmstopn  13249  mstopn  13250  bdxmet  13295  divcnap  13349  ivthinclemlr  13409  ivthinclemur  13411  dvlemap  13443  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471  dveflem  13481  lgsfle1  13704  lgsle1  13710  lgsdirprm  13729  lgsne0  13733  bj-indsuc  13963  nnsf  14038