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-3 7
ax-mp 8    &       =>   
wa 96
wb 97
ax-ia1 98
ax-ia2 99
ax-ia3 100
df-bi 109
ax-in1 527
ax-in2 528
wo 606
ax-io 607
w3o 902
w3a 903
df-3or 904
df-3an 905
ax-meredith 1251
wnand 1279
df-nand 1280
wtru 1310
wfal 1311
df-tru 1313
df-fal 1314
wal 1335
ax-5 1336
ax-6 1337
ax-7 1338
ax-gen 1339    =>   
wex 1374
ax-ie1 1375
ax-ie2 1376
cv 1382
wceq 1383
wcel 1385
ax-8 1387
ax-10 1388
ax-11 1389
ax-i11e 1390
ax-i12 1391
ax-4 1392
ax-13 1395
ax-14 1396
ax-17 1402
ax-i9 1417
ax-5o 1425
ax-6o 1428
ax-ial 1430
ax-i5r 1431
ax-9o 1558
ax-10o 1576
wsbc 1604
df-sb 1606
ax-16 1644
ax-11o 1654
ax-15 1807
weu 1829
wmo 1830
df-eu 1833
df-mo 1834
  Copyright terms: Public domain W3C validator