hba1-o - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hba1-o		Structured version Unicode version

Theorem hba1-o 2228

Description:

is not free in

. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

**Assertion**
Ref	Expression
hba1-o

**Proof of Theorem hba1-o**
Step	Hyp	Ref	Expression
1		ax-4 2214	. . 3
2	1	con2i 115	. 2
3		ax6 2226	. 2
4		ax6 2226	. . . 4
5	4	con1i 124	. . 3
6	5	alimi 1569	. 2
7	2, 3, 6	3syl 19	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wal 1550

This theorem is referenced by: a5i-o 2229 nfa1-o 2245 ax67to6 2246 ax467to6 2250 dvelimf-o 2259 ax11indalem 2276 ax11inda2ALT 2277 ax11inda 2279

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1556 ax-5 1567 ax-4 2214 ax-5o 2215 ax-6o 2216

W3C validator