![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpli | Unicode version |
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
Ref | Expression |
---|---|
simpli.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
simpli |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpli.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simpl 108 |
. 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-ia1 105 |
This theorem is referenced by: bi1 117 bi2 129 dfbi2 386 orc 702 pwundifss 4215 ssdomg 6680 negiso 8737 infrenegsupex 9416 xrnegiso 11063 infxrnegsupex 11064 cos01bnd 11501 cos1bnd 11502 cos2bnd 11503 sin4lt0 11509 egt2lt3 11522 epos 11523 ene1 11527 eap1 11528 slotslfn 12024 strslfvd 12039 strslfv2d 12040 strsl0 12046 setsslid 12048 setsslnid 12049 reeff1o 12902 pigt2lt4 12913 pire 12915 pipos 12917 sinhalfpi 12925 tan4thpi 12970 sincos3rdpi 12972 pigt3 12973 |
Copyright terms: Public domain | W3C validator |