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 527
ax-in2 528
wo 608
ax-io 609
wdc 717 DECID
df-dc 718 DECID
w3o 842
w3a 843
df-3or 844
df-3an 845
wtru 1187
wfal 1188
df-tru 1190
df-fal 1191
wxo 1206  \/_
df-xor 1207  \/_
wal 1266
ax-5 1267
ax-7 1268
ax-gen 1269    =>   
wnf 1280 
F/
df-nf 1281  F/
wex 1313
ax-ie1 1314
ax-ie2 1315
cv 1323
wceq 1324
wcel 1326
ax-8 1328
ax-10 1329
ax-11 1330
ax-i12 1331
ax-bnd 1332
ax-4 1333
ax-13 1337
ax-14 1338
ax-17 1350
ax-i9 1354
ax-ial 1359
ax-i5r 1360
ax-10o 1494
wsbc 1531
df-sb 1533
ax-16 1581
ax-11o 1590
ax-ext 1775
cab 1778  {  |  }
df-clab 1779  {  |  }
df-cleq 1785    =>   
df-clel 1788
wnfc 1915  F/_
df-nfc 1917  F/_  F/
wne 1954  =/=
wnel 1955  e/
df-ne 1956  =/=
df-nel 1957  e/
ax-3 2039
weu 2075
wmo 2076
df-eu 2079
df-mo 2080
  Copyright terms: Public domain W3C validator