![]() |
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 109 |
. 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 106 |
This theorem is referenced by: biimp 118 biimpr 130 dfbi2 388 orc 712 pwundifss 4285 ssdomg 6777 negiso 8911 infrenegsupex 9593 xrnegiso 11269 infxrnegsupex 11270 cos01bnd 11765 cos1bnd 11766 cos2bnd 11767 sin4lt0 11773 egt2lt3 11786 epos 11787 ene1 11791 eap1 11792 slotslfn 12487 strslfvd 12503 strslfv2d 12504 strsl0 12510 setsslid 12512 setsslnid 12513 reeff1o 14164 pigt2lt4 14175 pire 14177 pipos 14179 sinhalfpi 14187 tan4thpi 14232 sincos3rdpi 14234 pigt3 14235 lgsdir2lem4 14402 lgsdir2lem5 14403 |
Copyright terms: Public domain | W3C validator |