ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simprbi Unicode version

Theorem simprbi 260
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
StepHypRef Expression
1 simprbi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpi 113 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 107 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm5.63dc  853  sb1  1649  reurmo  2524  pssne  3040  pssn2lp  3045  ssnpss  3047  eldifn  3067  disj4im  3276  rabsnt  3445  eldifsni  3496  unimax  3614  ssintub  3633  moop2  3988  wepo  4096  wetrep  4097  trssord  4117  ordelord  4118  ordsucim  4226  ordtri2or2exmidlem  4251  regexmidlem1  4258  reg2exmidlema  4259  tfis  4306  opelxp2  4378  funmo  4917  funopg  4934  funco  4940  funun  4944  fununi  4967  funimaexglem  4982  fndm  4998  frn  5052  f1ss  5097  f1ssr  5098  f1ssres  5099  forn  5109  f1f1orn  5137  f1orescnv  5142  f1imacnv  5143  funcocnv2  5151  funfveu  5188  nfvres  5206  foelrn  5317  isorel  5448  isoini2  5458  f1ofveu  5500  fovcl  5606  f1opw  5707  f1o2ndf1  5849  mpt2xopn0yelv  5854  swoer  6134  en0  6275  en1  6279  phplem4  6318  phplem4dom  6324  phplem4on  6329  ssfiexmid  6336  diffitest  6344  0npi  6411  mulclpi  6426  mulcanpig  6433  nlt1pig  6439  indpi  6440  nnppipi  6441  dfplpq2  6452  archnqq  6515  enq0tr  6532  nqnq0pi  6536  ltexprlemopl  6699  ltexprlemopu  6701  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemupu  6747  cauappcvgprlemdisj  6749  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemupu  6770  caucvgprlemdisj  6772  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemupu  6798  caucvgprprlemdisj  6800  ltresr2  6916  peano2nnnn  6929  axrnegex  6953  ltxrlt  7085  peano2nn  7926  elnn0z  8258  zaddcl  8285  ztri3or0  8287  1nuz2  8543  rpgt0  8594  ixxss1  8773  ixxss2  8774  ixxss12  8775  iccss2  8813  iccssico2  8816  elfzuz3  8887  uzdisj  8955  nn0disj  8995  serige0  9252  expge0  9291  expge1  9292  expaddzaplem  9298  shftfn  9425  bj-indsuc  10052
  Copyright terms: Public domain W3C validator