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

Theorem simpri 112
 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 109 . 2 ((𝜑𝜓) → 𝜓)
31, 2ax-mp 5 1 𝜓
 Colors of variables: wff set class Syntax hints:   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-ia2 106 This theorem is referenced by:  bi3  118  dfbi2  386  olc  701  mptxor  1403  sb4bor  1808  ordsoexmid  4486  eninl  6992  eninr  6993  pw1ne1  7100  negiso  8757  infrenegsupex  9436  xrnegiso  11083  infxrnegsupex  11084  cos01bnd  11521  cos1bnd  11522  cos2bnd  11523  sincos2sgn  11528  sin4lt0  11529  egt2lt3  11542  slotslfn  12044  strslfvd  12059  strslfv2d  12060  strslfv  12062  strsl0  12066  setsslid  12068  setsslnid  12069  rngplusgg  12135  rngmulrg  12136  srngplusgd  12142  srngmulrd  12143  srnginvld  12144  lmodplusgd  12153  lmodscad  12154  lmodvscad  12155  ipsaddgd  12161  ipsmulrd  12162  ipsscad  12163  ipsvscad  12164  ipsipd  12165  topgrpplusgd  12171  topgrptsetd  12172  setsmsdsg  12708  cosz12  12929  sinpi  12934  sinhalfpilem  12940  coshalfpi  12946  sincosq1lem  12974  tangtx  12987  sincos4thpi  12989  tan4thpi  12990  sincos6thpi  12991  sincos3rdpi  12992  pigt3  12993  logltb  13023
 Copyright terms: Public domain W3C validator