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, 24-Jan-1993.) (New usage is discouraged.)

Assertion

Ref	Expression
hba1-o

Proof of Theorem hba1-o

Step	Hyp	Ref	Expression
1		ax-c5 2214	. . 3
2	1	con2i 120	. 2
3		ax10 2226	. 2
4		ax10 2226	. . . 4
5	4	con1i 129	. . 3
6	5	alimi 1633	. 2
7	2, 3, 6	3syl 20	1

Syntax hints:  -.wn 3  ->wi 4  A.wal 1393

This theorem is referenced by:  axc4i-o  2229  nfa1-o  2245  axc711toc7  2246  axc5c711toc7  2250  dvelimf-o  2259  ax12indalem  2275  ax12inda2ALT  2276  ax12inda  2278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-c5 2214  ax-c4 2215  ax-c7 2216