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

Theorem simprbi 273
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 119 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 113 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.63dc  915  sb1  1724  reurmo  2622  eldifn  3169  elinel2  3233  rabsnt  3568  eldifsni  3622  unimax  3740  ssintub  3759  exmidsssnc  4096  moop2  4143  wepo  4251  wetrep  4252  trssord  4272  ordelord  4273  ordsucim  4386  ordtri2or2exmidlem  4411  regexmidlem1  4418  reg2exmidlema  4419  tfis  4467  opelxp2  4544  funmo  5108  funopg  5127  funco  5133  funun  5137  fununi  5161  funimaexglem  5176  fndm  5192  frn  5251  f1ss  5304  f1ssr  5305  f1ssres  5307  forn  5318  f1f1orn  5346  f1orescnv  5351  f1imacnv  5352  funcocnv2  5360  funfveu  5402  nfvres  5422  isorel  5677  isoini2  5688  f1ofveu  5730  fovcl  5844  f1opw  5945  f1o2ndf1  6093  mpoxopn0yelv  6104  swoer  6425  mapsnconst  6556  en0  6657  en1  6661  phplem4  6717  phplem4dom  6724  phplem4on  6729  ssfilem  6737  diffitest  6749  inffiexmid  6768  supubti  6854  suplubti  6855  djuinr  6916  casefun  6938  casef1  6943  djufun  6957  ctssexmid  6992  exmidonfinlem  7017  exmidfodomrlemim  7025  0npi  7089  mulclpi  7104  mulcanpig  7111  nlt1pig  7117  indpi  7118  nnppipi  7119  dfplpq2  7130  archnqq  7193  enq0tr  7210  nqnq0pi  7214  ltexprlemopl  7377  ltexprlemopu  7379  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemopu  7424  cauappcvgprlemupu  7425  cauappcvgprlemdisj  7427  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemopu  7447  caucvgprlemupu  7448  caucvgprlemdisj  7450  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemupu  7476  caucvgprprlemdisj  7478  suplocsrlempr  7583  ltresr2  7616  peano2nnnn  7629  axrnegex  7655  ltxrlt  7798  peano2nn  8700  elnn0z  9035  zaddcl  9062  ztri3or0  9064  eluz2gt1  9364  1nuz2  9368  rpgt0  9421  ixxss1  9655  ixxss2  9656  ixxss12  9657  iccss2  9695  iccssico2  9698  elfzuz3  9771  uzdisj  9841  nn0disj  9883  addmodlteq  10139  expge0  10297  expge1  10298  expaddzaplem  10304  shftfn  10564  fsumf1o  11127  fsumge0  11196  zsupcllemstep  11565  bezoutlemzz  11617  bezoutlemaz  11618  bezoutlembz  11619  bezoutlemsup  11624  1nprm  11722  nprm  11731  sqnprm  11743  dvdsprm  11744  coprm  11749  sqpweven  11780  2sqpwodd  11781  dfphi2  11823  phimullem  11828  oddennn  11832  znnen  11838  ennnfonelemg  11843  ctinf  11870  toponuni  12109  tpsuni  12128  neipsm  12250  cnf  12300  cnima  12316  txdis1cn  12374  hmeocnvcn  12402  psmetxrge0  12428  isxmet2d  12444  xmstopn  12551  mstopn  12552  bdxmet  12597  divcnap  12651  ivthinclemlr  12711  ivthinclemur  12713  dvlemap  12745  dvcnp2cntop  12759  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  dvcjbr  12768  dvrecap  12773  dveflem  12782  bj-indsuc  13053  nnsf  13126  nninfalllemn  13129
  Copyright terms: Public domain W3C validator