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

Theorem simprbi 269
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 118 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 112 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.63dc  888  sb1  1690  reurmo  2569  eldifn  3096  elinel2  3160  rabsnt  3475  eldifsni  3526  unimax  3643  ssintub  3662  moop2  4014  wepo  4122  wetrep  4123  trssord  4143  ordelord  4144  ordsucim  4252  ordtri2or2exmidlem  4277  regexmidlem1  4284  reg2exmidlema  4285  tfis  4332  opelxp2  4404  funmo  4947  funopg  4964  funco  4970  funun  4974  fununi  4998  funimaexglem  5013  fndm  5029  frn  5083  f1ss  5128  f1ssr  5129  f1ssres  5130  forn  5140  f1f1orn  5168  f1orescnv  5173  f1imacnv  5174  funcocnv2  5182  funfveu  5219  nfvres  5238  foelrn  5349  isorel  5479  isoini2  5489  f1ofveu  5531  fovcl  5637  f1opw  5738  f1o2ndf1  5880  mpt2xopn0yelv  5888  swoer  6200  en0  6342  en1  6346  phplem4  6390  phplem4dom  6397  phplem4on  6402  ssfilem  6410  diffitest  6421  supubti  6471  suplubti  6472  0npi  6565  mulclpi  6580  mulcanpig  6587  nlt1pig  6593  indpi  6594  nnppipi  6595  dfplpq2  6606  archnqq  6669  enq0tr  6686  nqnq0pi  6690  ltexprlemopl  6853  ltexprlemopu  6855  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemupu  6901  cauappcvgprlemdisj  6903  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemupu  6924  caucvgprlemdisj  6926  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemupu  6952  caucvgprprlemdisj  6954  ltresr2  7070  peano2nnnn  7083  axrnegex  7107  ltxrlt  7245  peano2nn  8118  elnn0z  8445  zaddcl  8472  ztri3or0  8474  eluz2gt1  8770  1nuz2  8774  rpgt0  8826  ixxss1  9003  ixxss2  9004  ixxss12  9005  iccss2  9043  iccssico2  9046  elfzuz3  9118  uzdisj  9186  nn0disj  9225  addmodlteq  9480  serige0  9570  expge0  9609  expge1  9610  expaddzaplem  9616  shftfn  9850  zsupcllemstep  10485  bezoutlemzz  10535  bezoutlemaz  10536  bezoutlembz  10537  bezoutlemsup  10542  1nprm  10640  nprm  10649  sqnprm  10661  dvdsprm  10662  coprm  10667  sqpweven  10697  2sqpwodd  10698  oddennn  10703  znnen  10709  bj-indsuc  10881
  Copyright terms: Public domain W3C validator