Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpri | GIF version |
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
Ref | Expression |
---|---|
simpri.1 | ⊢ (𝜑 ∧ 𝜓) |
Ref | Expression |
---|---|
simpri | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpri.1 | . 2 ⊢ (𝜑 ∧ 𝜓) | |
2 | simpr 109 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
3 | 1, 2 | ax-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 385 olc 700 mptxor 1402 sb4bor 1807 ordsoexmid 4477 eninl 6982 eninr 6983 negiso 8713 infrenegsupex 9389 xrnegiso 11031 infxrnegsupex 11032 cos01bnd 11465 cos1bnd 11466 cos2bnd 11467 sincos2sgn 11472 sin4lt0 11473 egt2lt3 11486 slotslfn 11985 strslfvd 12000 strslfv2d 12001 strslfv 12003 strsl0 12007 setsslid 12009 setsslnid 12010 rngplusgg 12076 rngmulrg 12077 srngplusgd 12083 srngmulrd 12084 srnginvld 12085 lmodplusgd 12094 lmodscad 12095 lmodvscad 12096 ipsaddgd 12102 ipsmulrd 12103 ipsscad 12104 ipsvscad 12105 ipsipd 12106 topgrpplusgd 12112 topgrptsetd 12113 setsmsdsg 12649 cosz12 12861 sinpi 12866 sinhalfpilem 12872 coshalfpi 12878 sincosq1lem 12906 tangtx 12919 sincos4thpi 12921 tan4thpi 12922 sincos6thpi 12923 sincos3rdpi 12924 pigt3 12925 |
Copyright terms: Public domain | W3C validator |