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  6409  mulclpi  6424  mulcanpig  6431  nlt1pig  6437  indpi  6438  nnppipi  6439  dfplpq2  6450  archnqq  6513  enq0tr  6530  nqnq0pi  6534  ltexprlemopl  6697  ltexprlemopu  6699  cauappcvgprlemopl  6742  cauappcvgprlemlol  6743  cauappcvgprlemopu  6744  cauappcvgprlemupu  6745  cauappcvgprlemdisj  6747  caucvgprlemopl  6765  caucvgprlemlol  6766  caucvgprlemopu  6767  caucvgprlemupu  6768  caucvgprlemdisj  6770  caucvgprprlemopl  6793  caucvgprprlemlol  6794  caucvgprprlemopu  6795  caucvgprprlemupu  6796  caucvgprprlemdisj  6798  ltresr2  6914  peano2nnnn  6927  axrnegex  6951  ltxrlt  7083  peano2nn  7924  elnn0z  8256  zaddcl  8283  ztri3or0  8285  1nuz2  8541  rpgt0  8592  ixxss1  8771  ixxss2  8772  ixxss12  8773  iccss2  8811  iccssico2  8814  elfzuz3  8885  uzdisj  8953  nn0disj  8993  serige0  9226  expge0  9265  expge1  9266  expaddzaplem  9272  shftfn  9399  bj-indsuc  10026
  Copyright terms: Public domain W3C validator