Definition df-limpl 313

Description: Church-encoding of logical conjunction.

Assertion

Ref	Expression
df-limpl	⊦ Impl = λaλb(baTrue)

Distinct variable group:   a,b

Detailed syntax breakdown of Definition df-limpl

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

This definition is referenced by: (None)