Definition df-an 128

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

Assertion

Ref	Expression
df-an	⊢ ⊤⊧[ ∧ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]

Distinct variable group:   f,p,q

Detailed syntax breakdown of Definition df-an

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
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 [⊤f:(∗ → (∗ → ∗))⊤]
15	7, 8, 14	kl 6	. . . . . 6 term λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]
16		ke 7	. . . . . 6 term =
17	13, 15, 16	kbr 9	. . . . 5 term [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
18	3, 5, 17	kl 6	. . . 4 term λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
19	3, 4, 18	kl 6	. . 3 term λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
20	2, 19, 16	kbr 9	. 2 term [ ∧ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
21	1, 20	wffMMJ2 11	1 wff ⊤⊧[ ∧ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]

This definition is referenced by:  wan  136  anval  148