Higher-Order Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  dfan2		Unicode version

---

Theorem dfan2 144

Description: An alternative defintion of the "and" term in terms of the context conjunction.

Hypotheses

Ref	Expression
dfan2.1
dfan2.2

Assertion

Ref	Expression
dfan2

---

Proof of Theorem dfan2 Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wan 126	. . . . . 6
2		dfan2.1	. . . . . 6
3		dfan2.2	. . . . . 6
4	1, 2, 3	wov 64	. . . . 5
5	4	trud 27	. . . 4
6		wv 58	. . . . . . . 8
7	6, 2, 3	wov 64	. . . . . . 7
8	7	wl 59	. . . . . 6
9		wv 58	. . . . . . . 8
10	9	wl 59	. . . . . . 7
11	10	wl 59	. . . . . 6
12	8, 11	wc 45	. . . . 5
13	4	id 25	. . . . . . 7
14	2, 3	anval 138	. . . . . . . 8
15	4, 14	a1i 28	. . . . . . 7
16	13, 15	mpbi 72	. . . . . 6
17	8, 11, 16	ceq1 79	. . . . 5
18	6, 11	weqi 68	. . . . . . . . . 10
19	18	id 25	. . . . . . . . 9
20	6, 2, 3, 19	oveq 92	. . . . . . . 8
21	9, 2	weqi 68	. . . . . . . . . . 11
22	21	id 25	. . . . . . . . . 10
23		wv 58	. . . . . . . . . . . 12
24	23, 3	weqi 68	. . . . . . . . . . 11
25	24, 2	eqid 73	. . . . . . . . . 10
26	9, 2, 3, 22, 25	ovl 107	. . . . . . . . 9
27	18, 26	a1i 28	. . . . . . . 8
28	7, 20, 27	eqtri 85	. . . . . . 7
29	7, 11, 28	cl 106	. . . . . 6
30	4, 29	a1i 28	. . . . 5
31		wtru 40	. . . . . . . 8
32	6, 31, 31	wov 64	. . . . . . 7
33	6, 31, 31, 19	oveq 92	. . . . . . . 8
34	9, 31	weqi 68	. . . . . . . . . . 11
35	34	id 25	. . . . . . . . . 10
36	23, 31	weqi 68	. . . . . . . . . . 11
37	36, 31	eqid 73	. . . . . . . . . 10
38	9, 31, 31, 35, 37	ovl 107	. . . . . . . . 9
39	18, 38	a1i 28	. . . . . . . 8
40	32, 33, 39	eqtri 85	. . . . . . 7
41	32, 11, 40	cl 106	. . . . . 6
42	4, 41	a1i 28	. . . . 5
43	12, 17, 30, 42	3eqtr3i 87	. . . 4
44	5, 43	mpbir 77	. . 3
45	23	wl 59	. . . . . . 7
46	45	wl 59	. . . . . 6
47	8, 46	wc 45	. . . . 5
48	8, 46, 16	ceq1 79	. . . . 5
49	6, 46	weqi 68	. . . . . . . . . 10
50	49	id 25	. . . . . . . . 9
51	6, 2, 3, 50	oveq 92	. . . . . . . 8
52	7, 46, 51	cl 106	. . . . . . 7
53	21, 23	eqid 73	. . . . . . . . 9
54	24	id 25	. . . . . . . . 9
55	23, 2, 3, 53, 54	ovl 107	. . . . . . . 8
56	31, 55	a1i 28	. . . . . . 7
57	47, 52, 56	eqtri 85	. . . . . 6
58	4, 57	a1i 28	. . . . 5
59	6, 31, 31, 50	oveq 92	. . . . . . . 8
60	34, 23	eqid 73	. . . . . . . . . 10
61	36	id 25	. . . . . . . . . 10
62	23, 31, 31, 60, 61	ovl 107	. . . . . . . . 9
63	49, 62	a1i 28	. . . . . . . 8
64	32, 59, 63	eqtri 85	. . . . . . 7
65	32, 46, 64	cl 106	. . . . . 6
66	4, 65	a1i 28	. . . . 5
67	47, 48, 58, 66	3eqtr3i 87	. . . 4
68	5, 67	mpbir 77	. . 3
69	44, 68	jca 18	. 2
70	2, 3	simpl 22	. . . . . . 7
71	70	eqtru 76	. . . . . 6
72	2, 3	simpr 23	. . . . . . 7
73	72	eqtru 76	. . . . . 6
74	6, 31, 31, 71, 73	oveq12 90	. . . . 5
75	32, 74	eqcomi 70	. . . 4
76	7, 75	leq 81	. . 3
77	70	ax-cb1 29	. . . 4
78	77, 14	a1i 28	. . 3
79	76, 78	mpbir 77	. 2
80	69, 79	dedi 75	1

Colors of variables: type var term

Syntax hints:  tv 1   ht 2  hb 3  kc 5  kl 6   ke 7  kt 8  kbr 9  kct 10   wffMMJ2 11  wffMMJ2t 12   tan 109

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103

This theorem depends on definitions:  df-ov 65  df-an 118

This theorem is referenced by:  hbct  145  mpd  146  ex  148

Copyright terms: Public domain

W3C validator