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 206
[Hamilton] p. 73	Rule 1	axmp 193
[Hamilton] p. 74	Rule 2	axgen 197
[Margaris] p. 49	Axiom A1	ax1 190
[Margaris] p. 49	Axiom A2	ax2 191
[Margaris] p. 49	Axiom A3	ax3 192
[Margaris] p. 89	Theorem 19.7	alnex 174
[Margaris] p. 90	Theorem 19.14	exnal 188
[Margaris] p. 90	Theorem 19.20	alimdv 172
[Margaris] p. 90	Theorem 19.22	eximdv 173
[Megill] p. 444	Axiom C5	ax17 205
[Megill] p. 445	Lemma L12	ax10 200
[Megill] p. 448	Scheme C6'	ax7 196
[Megill] p. 448	Scheme C8'	ax8 198  ax9 199
[Megill] p. 448	Scheme C9'	ax12 202
[Megill] p. 448	Scheme C12'	ax13 203  ax14 204
[Monk2] p. 105	Axiom C4	ax5 194
[Monk2] p. 105	Axiom C7	ax8 198  ax9 199
[Monk2] p. 105	Axiom C8	ax11 201
[Monk2] p. 113	Axiom C5-1	ax17 205
[Monk2] p. 113	Axiom C5-2	ax6 195
[TakeutiZaring] p. 19	Axiom 5	axrep 207
[Tarski] p. 70	Lemma 16	ax11 201
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax17 205
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax13 203  ax14 204