Metamath Solitaire JS (build 9.0.1, August 11 2023)
Propositional calculus
ax1
ax2
ax3
axmp
dfbi1
dfbi2
dfbi3
dfor
dfan
Predicate calculus 1
axc5
ax4
axc4
ax10
ax11
axgen
dfex
dfeu
dfmo
dfnf
Predicate calculus 2
ax7
axc10
axc11
axc15
axc9
ax8
ax9
axc16
ax5
dfsb
Predicate calculus old
ax10a
axc7
ax6v
ax6
axc11n
ax12
ax13v
ax13
axc14
axextv
Set theory
axext
axrep
axun
axpow
axreg
axinf
axac
Set theory definitions
dfclab
dfcleq
dfclel
dfsub
dfun
dfin
dfnul
dfv
dfuni
dfint
dfpw
dfsn
dfpr
dfop
dfsuc
undo
redo
animation
prove stuff
delete top
swap top
save top
load
export top
export top d
import
import d
add assumption
toggle unicode
toggle varcolors
toggle reverse stack
toggle export full proofs
toggle wii u test
Metamath