Theorem ax12eq 38942

Description: Basis step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. 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 1870	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2		equid 2011	. . . . . . . 8 ⊢ 𝑥 = 𝑥
3	2	a1i 11	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑥)
4	3	ax-gen 1795	. . . . . 6 ⊢ ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)
5	4	a1i 11	. . . . 5 ⊢ (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥))
6		equequ1 2024	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑥 ↔ 𝑧 = 𝑥))
7		equequ2 2025	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑤))
8	6, 7	sylan9bb 509	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 = 𝑥 ↔ 𝑧 = 𝑤))
9	8	sps-o 38909	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 = 𝑥 ↔ 𝑧 = 𝑤))
10		nfa1-o 38916	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤)
11	9	imbi2d 340	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 = 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
12	10, 11	albid 2222	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
13	9, 12	imbi12d 344	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
14	13	adantr 480	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
15	5, 14	mpbii 233	. . . 4 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
16	15	exp32 420	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
17	1, 16	sylbir 235	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
18		equequ1 2024	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤))
19	18	ad2antll 729	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤))
20		axc9 2387	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)))
21	20	impcom 407	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
22	21	adantrr 717	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
23		equtrr 2021	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑥 = 𝑦 → 𝑥 = 𝑤))
24	23	alimi 1811	. . . . . . 7 ⊢ (∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤))
25	22, 24	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
26	19, 25	sylbid 240	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
27	26	adantll 714	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
28		equequ1 2024	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤))
29	28	sps-o 38909	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤))
30	29	imbi2d 340	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 = 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
31	30	dral2-o 38931	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
32	29, 31	imbi12d 344	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
33	32	ad2antrr 726	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
34	27, 33	mpbid 232	. . 3 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
35	34	exp32 420	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
36		equequ2 2025	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
37	36	ad2antll 729	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
38		axc9 2387	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
39	38	imp 406	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
40	39	adantrr 717	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
41	36	biimprcd 250	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑥 = 𝑦 → 𝑧 = 𝑥))
42	41	alimi 1811	. . . . . . 7 ⊢ (∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥))
43	40, 42	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
44	37, 43	sylbid 240	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
45	44	adantlr 715	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
46	7	sps-o 38909	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑤))
47	46	imbi2d 340	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 = 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
48	47	dral2-o 38931	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
49	46, 48	imbi12d 344	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
50	49	ad2antlr 727	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
51	45, 50	mpbid 232	. . 3 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
52	51	exp32 420	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
53		ax6ev 1969	. . . . 5 ⊢ ∃𝑢 𝑢 = 𝑤
54		ax6ev 1969	. . . . . . 7 ⊢ ∃𝑣 𝑣 = 𝑧
55		ax-1 6	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑢 → (𝑥 = 𝑦 → 𝑣 = 𝑢))
56	55	alrimiv 1927	. . . . . . . . . 10 ⊢ (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢))
57		equequ1 2024	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 = 𝑢 ↔ 𝑧 = 𝑢))
58		equequ2 2025	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑧 = 𝑢 ↔ 𝑧 = 𝑤))
59	57, 58	sylan9bb 509	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
60	59	adantl 481	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
61		dveeq2-o 38934	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
62		dveeq2-o 38934	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
63	61, 62	im2anan9 620	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
64	63	imp 406	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
65		19.26 1870	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
66	64, 65	sylibr 234	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤))
67		nfa1-o 38916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)
68	59	sps-o 38909	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
69	68	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
70	67, 69	albid 2222	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
71	66, 70	syl 17	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
72	60, 71	imbi12d 344	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
73	56, 72	mpbii 233	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
74	73	exp32 420	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
75	74	exlimdv 1933	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
76	54, 75	mpi 20	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
77	76	exlimdv 1933	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
78	53, 77	mpi 20	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
79	78	a1d 25	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
80	79	a1d 25	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
81	17, 35, 52, 80	4cases 1041	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177  ax-13 2377  ax-c5 38884  ax-c4 38885  ax-c7 38886  ax-c10 38887  ax-c11 38888  ax-c9 38891

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by: (None)