Theorem ax12eq 36955

Description: Basis step for constructing a substitution instance of ax-c15 36903 without using ax-c15 36903. 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 1873	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2		equid 2015	. . . . . . . 8 ⊢ 𝑥 = 𝑥
3	2	a1i 11	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑥)
4	3	ax-gen 1798	. . . . . 6 ⊢ ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)
5	4	a1i 11	. . . . 5 ⊢ (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥))
6		equequ1 2028	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑥 ↔ 𝑧 = 𝑥))
7		equequ2 2029	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑤))
8	6, 7	sylan9bb 510	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 = 𝑥 ↔ 𝑧 = 𝑤))
9	8	sps-o 36922	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 = 𝑥 ↔ 𝑧 = 𝑤))
10		nfa1-o 36929	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤)
11	9	imbi2d 341	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 = 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
12	10, 11	albid 2215	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
13	9, 12	imbi12d 345	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
14	13	adantr 481	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
15	5, 14	mpbii 232	. . . 4 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
16	15	exp32 421	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
17	1, 16	sylbir 234	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
18		equequ1 2028	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤))
19	18	ad2antll 726	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤))
20		axc9 2382	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)))
21	20	impcom 408	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
22	21	adantrr 714	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
23		equtrr 2025	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑥 = 𝑦 → 𝑥 = 𝑤))
24	23	alimi 1814	. . . . . . 7 ⊢ (∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤))
25	22, 24	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
26	19, 25	sylbid 239	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
27	26	adantll 711	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)))
28		equequ1 2028	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤))
29	28	sps-o 36922	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤))
30	29	imbi2d 341	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 = 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
31	30	dral2-o 36944	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
32	29, 31	imbi12d 345	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
33	32	ad2antrr 723	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
34	27, 33	mpbid 231	. . 3 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
35	34	exp32 421	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
36		equequ2 2029	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
37	36	ad2antll 726	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
38		axc9 2382	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
39	38	imp 407	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
40	39	adantrr 714	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
41	36	biimprcd 249	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑥 = 𝑦 → 𝑧 = 𝑥))
42	41	alimi 1814	. . . . . . 7 ⊢ (∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥))
43	40, 42	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
44	37, 43	sylbid 239	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
45	44	adantlr 712	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)))
46	7	sps-o 36922	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑤))
47	46	imbi2d 341	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 = 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
48	47	dral2-o 36944	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
49	46, 48	imbi12d 345	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
50	49	ad2antlr 724	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
51	45, 50	mpbid 231	. . 3 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
52	51	exp32 421	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
53		ax6ev 1973	. . . . 5 ⊢ ∃𝑢 𝑢 = 𝑤
54		ax6ev 1973	. . . . . . 7 ⊢ ∃𝑣 𝑣 = 𝑧
55		ax-1 6	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑢 → (𝑥 = 𝑦 → 𝑣 = 𝑢))
56	55	alrimiv 1930	. . . . . . . . . 10 ⊢ (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢))
57		equequ1 2028	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 = 𝑢 ↔ 𝑧 = 𝑢))
58		equequ2 2029	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑧 = 𝑢 ↔ 𝑧 = 𝑤))
59	57, 58	sylan9bb 510	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
60	59	adantl 482	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
61		dveeq2-o 36947	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
62		dveeq2-o 36947	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
63	61, 62	im2anan9 620	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
64	63	imp 407	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
65		19.26 1873	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
66	64, 65	sylibr 233	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤))
67		nfa1-o 36929	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)
68	59	sps-o 36922	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤))
69	68	imbi2d 341	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤)))
70	67, 69	albid 2215	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
71	66, 70	syl 17	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
72	60, 71	imbi12d 345	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
73	56, 72	mpbii 232	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
74	73	exp32 421	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
75	74	exlimdv 1936	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
76	54, 75	mpi 20	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
77	76	exlimdv 1936	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
78	53, 77	mpi 20	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))
79	78	a1d 25	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
80	79	a1d 25	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))))
81	17, 35, 52, 80	4cases 1038	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372  ax-c5 36897  ax-c4 36898  ax-c7 36899  ax-c10 36900  ax-c11 36901  ax-c9 36904

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787

This theorem is referenced by: (None)