Definition df-eqtru 303

Description: A shorthand way of saying that a church-encoded value is true. I would totally use this as a new typecode, so I could prove statements with ⊨ instead of ⊦, but it turns out that adds needless complexity (and mmj2 doesn't like it).

Assertion

Ref	Expression
df-eqtru	⊦ (P = True ⧟ ⊨ P)

Detailed syntax breakdown of Definition df-eqtru

Step	Hyp	Ref	Expression
1		np	. . 3 nilad P
2		ntru 297	. . 3 nilad True
3	1, 2	weq 246	. 2 wff P = True
4	1	weqtru 301	. 2 wff ⊨ P
5	3, 4	wlb 55	1 wff (P = True ⧟ ⊨ P)

This definition is referenced by: (None)