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

Theorem simprbi 275
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 120 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 114 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm5.63dc  946  sb1  1766  reurmo  2691  eldifn  3258  elinel2  3322  rabsnt  3666  eldifsni  3720  unimax  3841  ssintub  3860  exmidsssnc  4200  moop2  4247  wepo  4355  wetrep  4356  trssord  4376  ordelord  4377  ordsucim  4495  ordtri2or2exmidlem  4521  regexmidlem1  4528  reg2exmidlema  4529  tfis  4578  opelxp2  4657  funmo  5226  funopg  5245  funco  5251  funun  5255  fununi  5279  funimaexglem  5294  fndm  5310  frn  5369  f1ss  5422  f1ssr  5423  f1ssres  5425  forn  5436  f1f1orn  5467  f1orescnv  5472  f1imacnv  5473  funcocnv2  5481  funfveu  5523  nfvres  5543  isorel  5802  isoini2  5813  f1ofveu  5856  fovcl  5973  f1opw  6071  f1o2ndf1  6222  mpoxopn0yelv  6233  swoer  6556  mapsnconst  6687  en0  6788  en1  6792  phplem4  6848  phplem4dom  6855  phplem4on  6860  ssfilem  6868  diffitest  6880  inffiexmid  6899  supubti  6991  suplubti  6992  djuinr  7055  casefun  7077  casef1  7082  djufun  7096  nnnninfeq  7119  ctssexmid  7141  exmidonfinlem  7185  exmidfodomrlemim  7193  cc4f  7246  cc4n  7248  0npi  7290  mulclpi  7305  mulcanpig  7312  nlt1pig  7318  indpi  7319  nnppipi  7320  dfplpq2  7331  archnqq  7394  enq0tr  7411  nqnq0pi  7415  ltexprlemopl  7578  ltexprlemopu  7580  cauappcvgprlemopl  7623  cauappcvgprlemlol  7624  cauappcvgprlemopu  7625  cauappcvgprlemupu  7626  cauappcvgprlemdisj  7628  caucvgprlemopl  7646  caucvgprlemlol  7647  caucvgprlemopu  7648  caucvgprlemupu  7649  caucvgprlemdisj  7651  caucvgprprlemopl  7674  caucvgprprlemlol  7675  caucvgprprlemopu  7676  caucvgprprlemupu  7677  caucvgprprlemdisj  7679  suplocsrlempr  7784  ltresr2  7817  peano2nnnn  7830  axrnegex  7856  ltxrlt  8000  peano2nn  8907  elnn0z  9242  zaddcl  9269  ztri3or0  9271  eluz2gt1  9578  1nuz2  9582  rpgt0  9639  ixxss1  9878  ixxss2  9879  ixxss12  9880  iccss2  9918  iccssico2  9921  elfzuz3  9995  uzdisj  10066  nn0disj  10111  addmodlteq  10371  expge0  10529  expge1  10530  expaddzaplem  10536  shftfn  10804  fsumf1o  11369  fsumge0  11438  fprodf1o  11567  zsupcllemstep  11916  zsupssdc  11925  bezoutlemzz  11973  bezoutlemaz  11974  bezoutlembz  11975  bezoutlemsup  11980  1nprm  12084  nprm  12093  sqnprm  12106  dvdsprm  12107  coprm  12114  sqpweven  12145  2sqpwodd  12146  dfphi2  12190  phimullem  12195  eulerthlemrprm  12199  phisum  12210  expnprm  12321  1arith  12335  oddennn  12363  znnen  12369  ennnfonelemg  12374  ctinf  12401  mndid  12705  mhmf  12733  mhmlin  12735  mhm0  12736  grpinvex  12764  grplinv  12799  mulgz  12886  mulgdirlem  12889  mulgdir  12890  mulgass  12895  ablcmn  12909  cmncom  12919  crngmgp  13000  toponuni  13146  tpsuni  13165  neipsm  13287  cnf  13337  cnima  13353  txdis1cn  13411  hmeocnvcn  13439  psmetxrge0  13465  isxmet2d  13481  xmstopn  13588  mstopn  13589  bdxmet  13634  divcnap  13688  ivthinclemlr  13748  ivthinclemur  13750  dvlemap  13782  dvcnp2cntop  13796  dvaddxxbr  13798  dvmulxxbr  13799  dvcoapbr  13804  dvcjbr  13805  dvrecap  13810  dveflem  13820  lgsfle1  14043  lgsle1  14049  lgsdirprm  14068  lgsne0  14072  bj-indsuc  14302  nnsf  14377
  Copyright terms: Public domain W3C validator