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

Theorem simpri 112
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
simpri.1  |-  ( ph  /\ 
ps )
Assertion
Ref Expression
simpri  |-  ps

Proof of Theorem simpri
StepHypRef Expression
1 simpri.1 . 2  |-  ( ph  /\ 
ps )
2 simpr 109 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2ax-mp 7 1  |-  ps
Colors of variables: wff set class
Syntax hints:    /\ wa 103
This theorem was proved from axioms:  ax-mp 7  ax-ia2 106
This theorem is referenced by:  bi3  118  dfbi2  383  olc  683  mptxor  1383  sb4bor  1787  ordsoexmid  4435  eninl  6932  eninr  6933  negiso  8617  infrenegsupex  9285  xrnegiso  10917  infxrnegsupex  10918  cos01bnd  11310  cos1bnd  11311  cos2bnd  11312  sincos2sgn  11317  sin4lt0  11318  egt2lt3  11328  slotslfn  11822  strslfvd  11837  strslfv2d  11838  strslfv  11840  strsl0  11844  setsslid  11846  setsslnid  11847  rngplusgg  11913  rngmulrg  11914  srngplusgd  11920  srngmulrd  11921  srnginvld  11922  lmodplusgd  11931  lmodscad  11932  lmodvscad  11933  ipsaddgd  11939  ipsmulrd  11940  ipsscad  11941  ipsvscad  11942  ipsipd  11943  topgrpplusgd  11949  topgrptsetd  11950  setsmsdsg  12463
  Copyright terms: Public domain W3C validator