Bibliographic Cross-Reference - High-Order Logic Explorer

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the High-Order Logic Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular reference, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Bibliographic Cross-Reference for the Higher-Order Logic Explorer

Bibliographic Reference	Description	Higher-Order Logic Explorer Page(s)
[BellMachover] p. 461	Axiom Ext	axext 219
[Hamilton] p. 73	Rule 1	axmp 206
[Hamilton] p. 74	Rule 2	axgen 210
[Margaris] p. 49	Axiom A1	ax1 203
[Margaris] p. 49	Axiom A2	ax2 204
[Margaris] p. 49	Axiom A3	ax3 205
[Margaris] p. 89	Theorem 19.7	alnex 186
[Margaris] p. 90	Theorem 19.14	exnal 201
[Margaris] p. 90	Theorem 19.20	alimdv 184
[Margaris] p. 90	Theorem 19.22	eximdv 185
[Megill] p. 444	Axiom C5	ax17m 218
[Megill] p. 445	Lemma L12	ax10 213
[Megill] p. 448	Scheme C6'	ax7 209
[Megill] p. 448	Scheme C8'	ax8 211  ax9 212
[Megill] p. 448	Scheme C9'	ax12 215
[Megill] p. 448	Scheme C12'	ax13 216  ax14 217
[Monk2] p. 105	Axiom C4	ax5 207
[Monk2] p. 105	Axiom C7	ax8 211  ax9 212
[Monk2] p. 105	Axiom C8	ax11 214
[Monk2] p. 113	Axiom C5-1	ax17m 218
[Monk2] p. 113	Axiom C5-2	ax6 208
[TakeutiZaring] p. 19	Axiom 5	axrep 220
[Tarski] p. 70	Lemma 16	ax11 214
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax17m 218
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax13 216  ax14 217