Theorem ax12eq 33244

Description: Basis step for constructing a substitution instance of ax-c15 33192 without using ax-c15 33192. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax12eq	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))

Proof of Theorem ax12eq

Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.26 1786	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2		equid 1926	. . . . . . . 8 ⊢ 𝑥 = 𝑥
3	2	a1i 11	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑥)
4	3	ax-gen 1713	. . . . . 6 ⊢ ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)
5	4	a1i 11	. . . . 5 ⊢ (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥))
6		equequ1 1939	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑥 ↔ 𝑧 = 𝑥))
7		equequ2 1940	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑤))
8	6, 7	sylan9bb 732	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 = 𝑥 ↔ 𝑧 = 𝑤))
9	8	sps-o 33211	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 = 𝑥 ↔ 𝑧 = 𝑤))
10		nfa1-o 33218	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤)
11	9	imbi2d 329	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 = 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
12	10, 11	albid 2077	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
13	9, 12	imbi12d 333	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
14	13	adantr 480	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
15	5, 14	mpbii 222	. . . 4 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
16	15	exp32 629	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
17	1, 16	sylbir 224	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
18		equequ1 1939	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤))
19	18	ad2antll 761	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤))
20		axc9 2290	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)))
21	20	impcom 445	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
22	21	adantrr 749	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
23		equtrr 1936	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑥 = 𝑦 → 𝑥 = 𝑤))
24	23	alimi 1730	. . . . . . 7 ⊢ (∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤))
25	22, 24	syl6 34	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
26	19, 25	sylbid 229	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
27	26	adantll 746	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
28		equequ1 1939	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤))
29	28	sps-o 33211	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤))
30	29	imbi2d 329	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 = 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
31	30	dral2-o 33233	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
32	29, 31	imbi12d 333	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
33	32	ad2antrr 758	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
34	27, 33	mpbid 221	. . 3 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
35	34	exp32 629	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
36		equequ2 1940	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
37	36	ad2antll 761	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
38		axc9 2290	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
39	38	imp 444	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
40	39	adantrr 749	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
41	36	biimprcd 239	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑥 = 𝑦 → 𝑧 = 𝑥))
42	41	alimi 1730	. . . . . . 7 ⊢ (∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥))
43	40, 42	syl6 34	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
44	37, 43	sylbid 229	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
45	44	adantlr 747	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
46	7	sps-o 33211	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑤))
47	46	imbi2d 329	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 = 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
48	47	dral2-o 33233	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
49	46, 48	imbi12d 333	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
50	49	ad2antlr 759	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
51	45, 50	mpbid 221	. . 3 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
52	51	exp32 629	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
53		ax6ev 1877	. . . . 5 ⊢ ∃𝑢 𝑢 = 𝑤
54		ax6ev 1877	. . . . . . 7 ⊢ ∃𝑣 𝑣 = 𝑧
55		ax-1 6	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑢 → (𝑥 = 𝑦 → 𝑣 = 𝑢))
56	55	alrimiv 1842	. . . . . . . . . 10 ⊢ (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢))
57		equequ1 1939	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 = 𝑢 ↔ 𝑧 = 𝑢))
58		equequ2 1940	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑧 = 𝑢 ↔ 𝑧 = 𝑤))
59	57, 58	sylan9bb 732	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
60	59	adantl 481	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
61		dveeq2-o 33236	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
62		dveeq2-o 33236	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
63	61, 62	im2anan9 876	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
64	63	imp 444	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
65		19.26 1786	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
66	64, 65	sylibr 223	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤))
67		nfa1-o 33218	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)
68	59	sps-o 33211	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
69	68	imbi2d 329	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
70	67, 69	albid 2077	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
71	66, 70	syl 17	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
72	60, 71	imbi12d 333	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
73	56, 72	mpbii 222	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
74	73	exp32 629	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
75	74	exlimdv 1848	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
76	54, 75	mpi 20	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
77	76	exlimdv 1848	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
78	53, 77	mpi 20	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
79	78	a1d 25	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
80	79	a1d 25	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
81	17, 35, 52, 80	4cases 987	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-c5 33186  ax-c4 33187  ax-c7 33188  ax-c10 33189  ax-c11 33190  ax-c9 33193

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by: (None)