Definition df-an 128

Description: Define the 'and' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
df-an	|- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]

Distinct variable group:   f,p,q

Detailed syntax breakdown of Definition df-an

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tan 119	. . 3 term /\
3		hb 3	. . . 4 type *
4		vp	. . . 4 var p
5		vq	. . . . 5 var q
6	3, 3	ht 2	. . . . . . . 8 type (* -> *)
7	3, 6	ht 2	. . . . . . 7 type (* -> (* -> *))
8		vf	. . . . . . 7 var f
9	3, 4	tv 1	. . . . . . . 8 term p:*
10	3, 5	tv 1	. . . . . . . 8 term q:*
11	7, 8	tv 1	. . . . . . . 8 term f:(* -> (* -> *))
12	9, 10, 11	kbr 9	. . . . . . 7 term [p:*f:(* -> (* -> *))q:*]
13	7, 8, 12	kl 6	. . . . . 6 term \f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*]
14	1, 1, 11	kbr 9	. . . . . . 7 term [T.f:(* -> (* -> *))T.]
15	7, 8, 14	kl 6	. . . . . 6 term \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]
16		ke 7	. . . . . 6 term =
17	13, 15, 16	kbr 9	. . . . 5 term [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]
18	3, 5, 17	kl 6	. . . 4 term \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]
19	3, 4, 18	kl 6	. . 3 term \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]
20	2, 19, 16	kbr 9	. 2 term [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
21	1, 20	wffMMJ2 11	1 wff T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]

This definition is referenced by:  wan  136  anval  148