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 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 1413 sb4bor 1822 ordsoexmid 4533 eninl 7053 eninr 7054 pw1ne1 7176 negiso 8841 infrenegsupex 9523 xrnegiso 11189 infxrnegsupex 11190 cos01bnd 11685 cos1bnd 11686 cos2bnd 11687 sincos2sgn 11692 sin4lt0 11693 egt2lt3 11706 ssnnctlemct 12322 slotslfn 12363 strslfvd 12378 strslfv2d 12379 strslfv 12381 strsl0 12385 setsslid 12387 setsslnid 12388 rngplusgg 12454 rngmulrg 12455 srngplusgd 12461 srngmulrd 12462 srnginvld 12463 lmodplusgd 12472 lmodscad 12473 lmodvscad 12474 ipsaddgd 12480 ipsmulrd 12481 ipsscad 12482 ipsvscad 12483 ipsipd 12484 topgrpplusgd 12490 topgrptsetd 12491 setsmsdsg 13027 cosz12 13248 sinpi 13253 sinhalfpilem 13259 coshalfpi 13265 sincosq1lem 13293 tangtx 13306 sincos4thpi 13308 tan4thpi 13309 sincos6thpi 13310 sincos3rdpi 13311 pigt3 13312 logltb 13342 |
Copyright terms: Public domain | W3C validator |