ILE Home Intuitionistic Logic Explorer This is the GIF version.
Change to Unicode version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 3
wi 4
ax-1 5
ax-2 6
ax-mp 7    &       =>   
wa 95
wb 96
ax-ia1 97
ax-ia2 98
ax-ia3 99
df-bi 108
ax-in1 526
ax-in2 527
wo 605
ax-io 606
ax-3 714
w3o 843
w3a 844
df-3or 845
df-3an 846
wtru 1189
wfal 1190
df-tru 1192
df-fal 1193
wal 1214
ax-5 1215
ax-6 1216
ax-7 1217
ax-gen 1218    =>   
wex 1253
ax-ie1 1254
ax-ie2 1255
cv 1261
wceq 1262
wcel 1264
ax-8 1266
ax-10 1267
ax-11 1268
ax-i11e 1269
ax-i12 1270
ax-4 1271
ax-13 1274
ax-14 1275
ax-17 1280
ax-i9 1282
ax-5o 1288
ax-6o 1291
ax-ial 1293
ax-i5r 1294
ax-9o 1391
ax-10o 1406
wsbc 1436
df-sb 1438
ax-16 1481
ax-11o 1491
ax-15 1660
weu 1669
wmo 1670
df-eu 1673
df-mo 1674
  Copyright terms: Public domain W3C validator