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 )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.63dc  948  sb1  1788  reurmo  2724  eldifn  3295  elinel2  3359  rabsnt  3707  eldifsni  3761  unimax  3883  ssintub  3902  exmidsssnc  4246  moop2  4294  wepo  4404  wetrep  4405  trssord  4425  ordelord  4426  ordsucim  4546  ordtri2or2exmidlem  4572  regexmidlem1  4579  reg2exmidlema  4580  tfis  4629  opelxp2  4708  funmo  5283  funopg  5302  funco  5308  funun  5312  fununi  5336  funimaexglem  5351  fndm  5367  frn  5428  f1ss  5481  f1ssr  5482  f1ssres  5484  forn  5495  f1f1orn  5527  f1orescnv  5532  f1imacnv  5533  funcocnv2  5541  funfveu  5583  nfvres  5604  isorel  5867  isoini2  5878  f1ofveu  5922  fovcld  6040  f1opw  6143  f1o2ndf1  6304  mpoxopn0yelv  6315  swoer  6638  mapsnconst  6771  en0  6872  en1  6876  phplem4  6934  phplem4dom  6941  phplem4on  6946  ssfilem  6954  diffitest  6966  inffiexmid  6985  supubti  7083  suplubti  7084  djuinr  7147  casefun  7169  casef1  7174  djufun  7188  nnnninfeq  7212  ctssexmid  7234  exmidonfinlem  7283  exmidfodomrlemim  7291  cc4f  7363  cc4n  7365  0npi  7408  mulclpi  7423  mulcanpig  7430  nlt1pig  7436  indpi  7437  nnppipi  7438  dfplpq2  7449  archnqq  7512  enq0tr  7529  nqnq0pi  7533  ltexprlemopl  7696  ltexprlemopu  7698  cauappcvgprlemopl  7741  cauappcvgprlemlol  7742  cauappcvgprlemopu  7743  cauappcvgprlemupu  7744  cauappcvgprlemdisj  7746  caucvgprlemopl  7764  caucvgprlemlol  7765  caucvgprlemopu  7766  caucvgprlemupu  7767  caucvgprlemdisj  7769  caucvgprprlemopl  7792  caucvgprprlemlol  7793  caucvgprprlemopu  7794  caucvgprprlemupu  7795  caucvgprprlemdisj  7797  suplocsrlempr  7902  ltresr2  7935  peano2nnnn  7948  axrnegex  7974  ltxrlt  8120  peano2nn  9030  elnn0z  9367  zaddcl  9394  ztri3or0  9396  eluz2gt1  9705  1nuz2  9709  rpgt0  9769  ixxss1  10008  ixxss2  10009  ixxss12  10010  iccss2  10048  iccssico2  10051  elfzuz3  10126  uzdisj  10197  nn0disj  10242  zsupcllemstep  10353  zsupssdc  10362  addmodlteq  10524  expge0  10701  expge1  10702  expaddzaplem  10708  shftfn  11054  fsumf1o  11620  fsumge0  11689  fprodf1o  11818  bitsfzolem  12184  bezoutlemzz  12242  bezoutlemaz  12243  bezoutlembz  12244  bezoutlemsup  12249  1nprm  12355  nprm  12364  sqnprm  12377  dvdsprm  12378  coprm  12385  sqpweven  12416  2sqpwodd  12417  dfphi2  12461  phimullem  12466  eulerthlemrprm  12470  phisum  12482  expnprm  12595  1arith  12609  4sqlem18  12650  oddennn  12682  znnen  12688  ennnfonelemg  12693  ctinf  12720  mndid  13175  mhmf  13215  mhmlin  13217  mhm0  13218  grpinvex  13260  grplinv  13300  mulgz  13404  mulgdirlem  13407  mulgdir  13408  mulgass  13413  nsgbi  13458  nmzbi  13463  ghmf  13501  ghmlin  13502  conjnsg  13535  ablcmn  13545  cmncom  13556  crngmgp  13684  rhmmhm  13839  rhmghm  13842  rimf1o  13850  nzrnz  13862  subrgss  13902  subrg1cl  13909  rrgeq0i  13944  domneq0  13952  2idlelbas  14196  2idlcpblrng  14203  znidomb  14338  toponuni  14405  tpsuni  14424  neipsm  14544  cnf  14594  cnima  14610  txdis1cn  14668  hmeocnvcn  14696  psmetxrge0  14722  isxmet2d  14738  xmstopn  14845  mstopn  14846  bdxmet  14891  divcnap  14955  ivthinclemlr  15027  ivthinclemur  15029  dvlemap  15070  dvcnp2cntop  15089  dvaddxxbr  15091  dvmulxxbr  15092  dvcoapbr  15097  dvcjbr  15098  dvrecap  15103  dveflem  15116  plyf  15127  plyadd  15141  plymul  15142  plycn  15152  dvply2g  15156  dvdsppwf1o  15379  mpodvdsmulf1o  15380  lgsfle1  15404  lgsle1  15410  lgsdirprm  15429  lgsne0  15433  lgsquadlem1  15472  lgsquadlem2  15473  bj-indsuc  15728  nnsf  15806