![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpri | Unicode 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 110 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
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 4561 eninl 7095 eninr 7096 pw1ne1 7227 negiso 8910 infrenegsupex 9592 xrnegiso 11265 infxrnegsupex 11266 cos01bnd 11761 cos1bnd 11762 cos2bnd 11763 sincos2sgn 11768 sin4lt0 11769 egt2lt3 11782 ssnnctlemct 12441 slotslfn 12482 strslfvd 12498 strslfv2d 12499 strslfv 12501 strsl0 12505 setsslid 12507 setsslnid 12508 rngplusgg 12589 rngmulrg 12590 srngplusgd 12600 srngmulrd 12601 srnginvld 12602 lmodplusgd 12618 lmodscad 12619 lmodvscad 12620 ipsaddgd 12630 ipsmulrd 12631 ipsscad 12632 ipsvscad 12633 ipsipd 12634 topgrpplusgd 12647 topgrptsetd 12648 imasex 12708 imasival 12709 imasbas 12710 imasplusg 12711 imasmulr 12712 fnmgp 13085 mgpvalg 13086 mgpex 13088 mgpbasg 13089 mgpscag 13090 mgptsetg 13091 mgpdsg 13093 mgpress 13094 ring1 13189 opprvalg 13194 opprex 13198 opprsllem 13199 setsmsdsg 13873 cosz12 14094 sinpi 14099 sinhalfpilem 14105 coshalfpi 14111 sincosq1lem 14139 tangtx 14152 sincos4thpi 14154 tan4thpi 14155 sincos6thpi 14156 sincos3rdpi 14157 pigt3 14158 logltb 14188 lgsdir2lem4 14325 lgsdir2lem5 14326 |
Copyright terms: Public domain | W3C validator |