Definition df-im 129

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

Assertion

Ref	Expression
df-im	|- T. |= [ ==> = \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 T.
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 T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]

This definition is referenced by:  wim  137  imval  146