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  890  sb1  1693  reurmo  2577  eldifn  3112  elinel2  3176  rabsnt  3500  eldifsni  3552  unimax  3670  ssintub  3689  moop2  4051  wepo  4159  wetrep  4160  trssord  4180  ordelord  4181  ordsucim  4289  ordtri2or2exmidlem  4314  regexmidlem1  4321  reg2exmidlema  4322  tfis  4370  opelxp2  4443  funmo  4993  funopg  5010  funco  5016  funun  5020  fununi  5044  funimaexglem  5059  fndm  5075  frn  5130  f1ss  5179  f1ssr  5180  f1ssres  5182  forn  5193  f1f1orn  5221  f1orescnv  5226  f1imacnv  5227  funcocnv2  5235  funfveu  5275  nfvres  5294  foelrnOLD  5487  isorel  5542  isoini2  5553  f1ofveu  5595  fovcl  5701  f1opw  5802  f1o2ndf1  5944  mpt2xopn0yelv  5952  swoer  6266  mapsnconst  6397  en0  6458  en1  6462  phplem4  6517  phplem4dom  6524  phplem4on  6529  ssfilem  6537  diffitest  6549  inffiexmid  6568  supubti  6631  suplubti  6632  djuinr  6692  casefun  6713  casef1  6718  djufun  6721  exmidfodomrlemim  6764  0npi  6809  mulclpi  6824  mulcanpig  6831  nlt1pig  6837  indpi  6838  nnppipi  6839  dfplpq2  6850  archnqq  6913  enq0tr  6930  nqnq0pi  6934  ltexprlemopl  7097  ltexprlemopu  7099  cauappcvgprlemopl  7142  cauappcvgprlemlol  7143  cauappcvgprlemopu  7144  cauappcvgprlemupu  7145  cauappcvgprlemdisj  7147  caucvgprlemopl  7165  caucvgprlemlol  7166  caucvgprlemopu  7167  caucvgprlemupu  7168  caucvgprlemdisj  7170  caucvgprprlemopl  7193  caucvgprprlemlol  7194  caucvgprprlemopu  7195  caucvgprprlemupu  7196  caucvgprprlemdisj  7198  ltresr2  7314  peano2nnnn  7327  axrnegex  7351  ltxrlt  7489  peano2nn  8362  elnn0z  8689  zaddcl  8716  ztri3or0  8718  eluz2gt1  9014  1nuz2  9018  rpgt0  9070  ixxss1  9247  ixxss2  9248  ixxss12  9249  iccss2  9287  iccssico2  9290  elfzuz3  9362  uzdisj  9430  nn0disj  9470  addmodlteq  9726  serige0  9843  expge0  9882  expge1  9883  expaddzaplem  9889  shftfn  10147  fsumf1o  10661  zsupcllemstep  10808  bezoutlemzz  10858  bezoutlemaz  10859  bezoutlembz  10860  bezoutlemsup  10865  1nprm  10963  nprm  10972  sqnprm  10984  dvdsprm  10985  coprm  10990  sqpweven  11020  2sqpwodd  11021  dfphi2  11063  phimullem  11068  oddennn  11072  znnen  11078  bj-indsuc  11253  nnsf  11325  nninfalllemn  11328
  Copyright terms: Public domain W3C validator