Definition df-im 129

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

Assertion

Ref	Expression
df-im	⊢ ⊤⊧[ ⇒ = λp:∗ λq:∗ [[p:∗ ∧ q:∗] = p:∗]]

Distinct variable group:   p,q

Detailed syntax breakdown of Definition df-im

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tim 121	. . 3 term ⇒
3		hb 3	. . . 4 type ∗
4		vp	. . . 4 var p
5		vq	. . . . 5 var q
6	3, 4	tv 1	. . . . . . 7 term p:∗
7	3, 5	tv 1	. . . . . . 7 term q:∗
8		tan 119	. . . . . . 7 term ∧
9	6, 7, 8	kbr 9	. . . . . 6 term [p:∗ ∧ q:∗]
10		ke 7	. . . . . 6 term =
11	9, 6, 10	kbr 9	. . . . 5 term [[p:∗ ∧ q:∗] = p:∗]
12	3, 5, 11	kl 6	. . . 4 term λq:∗ [[p:∗ ∧ q:∗] = p:∗]
13	3, 4, 12	kl 6	. . 3 term λp:∗ λq:∗ [[p:∗ ∧ q:∗] = p:∗]
14	2, 13, 10	kbr 9	. 2 term [ ⇒ = λp:∗ λq:∗ [[p:∗ ∧ q:∗] = p:∗]]
15	1, 14	wffMMJ2 11	1 wff ⊤⊧[ ⇒ = λp:∗ λq:∗ [[p:∗ ∧ q:∗] = p:∗]]

This definition is referenced by:  wim  137  imval  146