Definition df-o3 54

Description: Defined disjunction. (Contributed by NM, 2-Nov-1997.)

Assertion

Ref	Expression
df-o3	(a ∪3 b) = (a⊥ →3 (a⊥ →3 b))

Detailed syntax breakdown of Definition df-o3

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wo3 25	. 2 term  (a ∪3 b)
4	1	wn 4	. . 3 term  a⊥
5	4, 2	wi3 14	. . 3 term  (a⊥ →3 b)
6	4, 5	wi3 14	. 2 term  (a⊥ →3 (a⊥ →3 b))
7	3, 6	wb 1	1 wff  (a ∪3 b) = (a⊥ →3 (a⊥ →3 b))

This definition is referenced by: (None)