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  931  sb1  1740  reurmo  2648  eldifn  3203  elinel2  3267  rabsnt  3605  eldifsni  3659  unimax  3777  ssintub  3796  exmidsssnc  4133  moop2  4180  wepo  4288  wetrep  4289  trssord  4309  ordelord  4310  ordsucim  4423  ordtri2or2exmidlem  4448  regexmidlem1  4455  reg2exmidlema  4456  tfis  4504  opelxp2  4581  funmo  5145  funopg  5164  funco  5170  funun  5174  fununi  5198  funimaexglem  5213  fndm  5229  frn  5288  f1ss  5341  f1ssr  5342  f1ssres  5344  forn  5355  f1f1orn  5385  f1orescnv  5390  f1imacnv  5391  funcocnv2  5399  funfveu  5441  nfvres  5461  isorel  5716  isoini2  5727  f1ofveu  5769  fovcl  5883  f1opw  5984  f1o2ndf1  6132  mpoxopn0yelv  6143  swoer  6464  mapsnconst  6595  en0  6696  en1  6700  phplem4  6756  phplem4dom  6763  phplem4on  6768  ssfilem  6776  diffitest  6788  inffiexmid  6807  supubti  6893  suplubti  6894  djuinr  6955  casefun  6977  casef1  6982  djufun  6996  ctssexmid  7031  exmidonfinlem  7065  exmidfodomrlemim  7073  cc4f  7100  cc4n  7102  0npi  7144  mulclpi  7159  mulcanpig  7166  nlt1pig  7172  indpi  7173  nnppipi  7174  dfplpq2  7185  archnqq  7248  enq0tr  7265  nqnq0pi  7269  ltexprlemopl  7432  ltexprlemopu  7434  cauappcvgprlemopl  7477  cauappcvgprlemlol  7478  cauappcvgprlemopu  7479  cauappcvgprlemupu  7480  cauappcvgprlemdisj  7482  caucvgprlemopl  7500  caucvgprlemlol  7501  caucvgprlemopu  7502  caucvgprlemupu  7503  caucvgprlemdisj  7505  caucvgprprlemopl  7528  caucvgprprlemlol  7529  caucvgprprlemopu  7530  caucvgprprlemupu  7531  caucvgprprlemdisj  7533  suplocsrlempr  7638  ltresr2  7671  peano2nnnn  7684  axrnegex  7710  ltxrlt  7853  peano2nn  8755  elnn0z  9090  zaddcl  9117  ztri3or0  9119  eluz2gt1  9422  1nuz2  9426  rpgt0  9481  ixxss1  9716  ixxss2  9717  ixxss12  9718  iccss2  9756  iccssico2  9759  elfzuz3  9833  uzdisj  9903  nn0disj  9945  addmodlteq  10201  expge0  10359  expge1  10360  expaddzaplem  10366  shftfn  10627  fsumf1o  11190  fsumge0  11259  zsupcllemstep  11672  bezoutlemzz  11724  bezoutlemaz  11725  bezoutlembz  11726  bezoutlemsup  11731  1nprm  11829  nprm  11838  sqnprm  11850  dvdsprm  11851  coprm  11856  sqpweven  11887  2sqpwodd  11888  dfphi2  11930  phimullem  11935  oddennn  11939  znnen  11945  ennnfonelemg  11950  ctinf  11977  toponuni  12219  tpsuni  12238  neipsm  12360  cnf  12410  cnima  12426  txdis1cn  12484  hmeocnvcn  12512  psmetxrge0  12538  isxmet2d  12554  xmstopn  12661  mstopn  12662  bdxmet  12707  divcnap  12761  ivthinclemlr  12821  ivthinclemur  12823  dvlemap  12855  dvcnp2cntop  12869  dvaddxxbr  12871  dvmulxxbr  12872  dvcoapbr  12877  dvcjbr  12878  dvrecap  12883  dveflem  12893  bj-indsuc  13295  nnsf  13372  nninfalllemn  13375
  Copyright terms: Public domain W3C validator