Definition df-lor 315

Description: Church-encoding of logical disjunction.

Assertion

Ref	Expression
df-lor	⊦ Or = λaλb(Trueab)

Distinct variable group:   a,b

Detailed syntax breakdown of Definition df-lor

Step	Hyp	Ref	Expression
1		nlor 310	. 2 nilad Or
2		va	. . 3 var a
3		vb	. . . 4 var b
4		ntru 297	. . . . 5 nilad True
5	3	nvar 203	. . . . 5 nilad b
6	2	nvar 203	. . . . 5 nilad a
7	4, 5, 6	nov 284	. . . 4 nilad (Trueab)
8	3, 7	nla 279	. . 3 nilad λb(Trueab)
9	2, 8	nla 279	. 2 nilad λaλb(Trueab)
10	1, 9	weq 246	1 wff Or = λaλb(Trueab)

This definition is referenced by: (None)