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

Theorem simpri 113
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
simpri.1 (𝜑𝜓)
Assertion
Ref Expression
simpri 𝜓

Proof of Theorem simpri
StepHypRef Expression
1 simpri.1 . 2 (𝜑𝜓)
2 simpr 110 . 2 ((𝜑𝜓) → 𝜓)
31, 2ax-mp 5 1 𝜓
Colors of variables: wff set class
Syntax hints:  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-ia2 107
This theorem is referenced by:  bi3  119  dfbi2  388  olc  711  mptxor  1424  sb4bor  1835  ordsoexmid  4558  eninl  7090  eninr  7091  pw1ne1  7222  negiso  8898  infrenegsupex  9580  xrnegiso  11251  infxrnegsupex  11252  cos01bnd  11747  cos1bnd  11748  cos2bnd  11749  sincos2sgn  11754  sin4lt0  11755  egt2lt3  11768  ssnnctlemct  12427  slotslfn  12468  strslfvd  12483  strslfv2d  12484  strslfv  12486  strsl0  12490  setsslid  12492  setsslnid  12493  rngplusgg  12571  rngmulrg  12572  srngplusgd  12578  srngmulrd  12579  srnginvld  12580  lmodplusgd  12592  lmodscad  12593  lmodvscad  12594  ipsaddgd  12600  ipsmulrd  12601  ipsscad  12602  ipsvscad  12603  ipsipd  12604  topgrpplusgd  12617  topgrptsetd  12618  fnmgp  12956  mgpvalg  12957  mgpex  12959  mgpbasg  12960  mgpscag  12961  mgptsetg  12962  mgpdsg  12964  ring1  13059  opprvalg  13063  opprex  13067  opprsllem  13068  setsmsdsg  13640  cosz12  13861  sinpi  13866  sinhalfpilem  13872  coshalfpi  13878  sincosq1lem  13906  tangtx  13919  sincos4thpi  13921  tan4thpi  13922  sincos6thpi  13923  sincos3rdpi  13924  pigt3  13925  logltb  13955  lgsdir2lem4  14092  lgsdir2lem5  14093
  Copyright terms: Public domain W3C validator