pred
Top-level context.
Pure predicate calculus.
Theorems:
Name
Comment
19.24
19.25
19.38
19.39
2al.dfbi
2im.bldal
aaan
al-ex
al.andi
al.dfbi
al.ex
al.imdi
al.ordi
alan<
alan>
alcom
alexan<
alexan<<
alexan<>
alexan>
alexor
alexor-pre
aln.ex
alnan.ex
alor<
alor>
alrot4
ax6e
bexim
bexim<
bexim>
bi.bldald
bi.bldexd
bmpg<
bmpg>
bv-theor
bv-¬
bv-→
bv-↔
bv-∀
bv-∀b
bv-∃
bv-∃b
bv-∧
bv-∨
bvdef
bvdefd
bvsyl
eeor
eqt-∀
eqt-∀-i
eqt-∃
eqt-∃-i
ex.andi
ex.ordi
exalswap
exan-pre
exan.al
exan<
exan>
excom
excom13
excomim
exintr
exn.al
exor<
exor>
exrot3
exrot4
fv-alx
fv-aly
fv-alyd
fv-and
fv-bid
fv-exx
fv-exy
fv-exyd
fv-im
fv-imd
fv-imt
fv-nalx
fv-neg
fv-negd
fv-negt
fv-theor
fv.eqal
fv.eqex
fv.eqexd
fv.eqext
fvbi<
fvbi>
gen2
im.bldal
im.bldald
im.bldex
im.bldexd
im.bldext
imgen2>
imgen<
imgen<d
imgen<i
imgen<ri
imgen>
imgen>d
imgen>g
imgen>i
imgen>ri
mpg
naxgen
naxgend
qexmid
spec-ex
stdpc5