Definition df-land 314

Description: Church-encoding of logical conjunction.

Assertion

Ref	Expression
df-land	⊦ And = λaλb(baFalse)

Distinct variable group:   a,b

Detailed syntax breakdown of Definition df-land

Step	Hyp	Ref	Expression
1		nland 309	. 2 nilad And
2		va	. . 3 var a
3		vb	. . . 4 var b
4	3	nvar 203	. . . . 5 nilad b
5		nfal 298	. . . . 5 nilad False
6	2	nvar 203	. . . . 5 nilad a
7	4, 5, 6	nov 284	. . . 4 nilad (baFalse)
8	3, 7	nla 279	. . 3 nilad λb(baFalse)
9	2, 8	nla 279	. 2 nilad λaλb(baFalse)
10	1, 9	weq 246	1 wff And = λaλb(baFalse)

This definition is referenced by: (None)