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  952  sb1  1812  reurmo  2751  eldifn  3327  elinel2  3391  rabsnt  3741  eldifsni  3797  unimax  3922  ssintub  3941  exmidsssnc  4287  moop2  4338  wepo  4450  wetrep  4451  trssord  4471  ordelord  4472  ordsucim  4592  ordtri2or2exmidlem  4618  regexmidlem1  4625  reg2exmidlema  4626  tfis  4675  opelxp2  4754  funmo  5333  funopg  5352  funco  5358  funun  5362  fununi  5389  funimaexglem  5404  fndm  5420  frn  5482  f1ss  5539  f1ssr  5540  f1ssres  5542  forn  5553  f1f1orn  5585  f1orescnv  5590  f1imacnv  5591  funcocnv2  5599  funfveu  5642  nfvres  5665  isorel  5938  isoini2  5949  f1ofveu  5995  fovcld  6115  f1opw  6219  f1o2ndf1  6380  mpoxopn0yelv  6391  swoer  6716  mapsnconst  6849  en0  6955  en1  6959  phplem4  7024  phplem4dom  7031  phplem4on  7037  ssfilem  7045  diffitest  7057  inffiexmid  7079  supubti  7177  suplubti  7178  djuinr  7241  casefun  7263  casef1  7268  djufun  7282  nnnninfeq  7306  ctssexmid  7328  exmidonfinlem  7382  exmidfodomrlemim  7390  cc4f  7466  cc4n  7468  0npi  7511  mulclpi  7526  mulcanpig  7533  nlt1pig  7539  indpi  7540  nnppipi  7541  dfplpq2  7552  archnqq  7615  enq0tr  7632  nqnq0pi  7636  ltexprlemopl  7799  ltexprlemopu  7801  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemupu  7898  caucvgprprlemdisj  7900  suplocsrlempr  8005  ltresr2  8038  peano2nnnn  8051  axrnegex  8077  ltxrlt  8223  peano2nn  9133  elnn0z  9470  zaddcl  9497  ztri3or0  9499  eluz2gt1  9809  1nuz2  9813  rpgt0  9873  ixxss1  10112  ixxss2  10113  ixxss12  10114  iccss2  10152  iccssico2  10155  elfzuz3  10230  uzdisj  10301  nn0disj  10346  zsupcllemstep  10461  zsupssdc  10470  addmodlteq  10632  expge0  10809  expge1  10810  expaddzaplem  10816  shftfn  11350  fsumf1o  11916  fsumge0  11985  fprodf1o  12114  bitsfzolem  12480  bezoutlemzz  12538  bezoutlemaz  12539  bezoutlembz  12540  bezoutlemsup  12545  1nprm  12651  nprm  12660  sqnprm  12673  dvdsprm  12674  coprm  12681  sqpweven  12712  2sqpwodd  12713  dfphi2  12757  phimullem  12762  eulerthlemrprm  12766  phisum  12778  expnprm  12891  1arith  12905  4sqlem18  12946  oddennn  12978  znnen  12984  ennnfonelemg  12989  ctinf  13016  mndid  13473  mhmf  13513  mhmlin  13515  mhm0  13516  grpinvex  13558  grplinv  13598  mulgz  13702  mulgdirlem  13705  mulgdir  13706  mulgass  13711  nsgbi  13756  nmzbi  13761  ghmf  13799  ghmlin  13800  conjnsg  13833  ablcmn  13843  cmncom  13854  crngmgp  13982  rhmmhm  14138  rhmghm  14141  rimf1o  14149  nzrnz  14161  subrgss  14201  subrg1cl  14208  rrgeq0i  14243  domneq0  14251  2idlelbas  14495  2idlcpblrng  14502  znidomb  14637  toponuni  14704  tpsuni  14723  neipsm  14843  cnf  14893  cnima  14909  txdis1cn  14967  hmeocnvcn  14995  psmetxrge0  15021  isxmet2d  15037  xmstopn  15144  mstopn  15145  bdxmet  15190  divcnap  15254  ivthinclemlr  15326  ivthinclemur  15328  dvlemap  15369  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  dvrecap  15402  dveflem  15415  plyf  15426  plyadd  15440  plymul  15441  plycn  15451  dvply2g  15455  dvdsppwf1o  15678  mpodvdsmulf1o  15679  lgsfle1  15703  lgsle1  15709  lgsdirprm  15728  lgsne0  15732  lgsquadlem1  15771  lgsquadlem2  15772  upgr1or2  15916  umgredg2en  15924  lfgredg2dom  15945  upgr2wlkdc  16116  trlres  16128  bj-indsuc  16346  nnsf  16431