![]() |
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 109 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
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 |