Definition df-o3 53

Description: Defined disjunction.

Assertion

Ref	Expression
df-o3	(a u3 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 24	. 2 term (a u3 b)
4	1	wn 4	. . 3 term a_|_
5	4, 2	wi3 15	. . 3 term (a_|_ ->3 b)
6	4, 5	wi3 15	. 2 term (a_|_ ->3 (a_|_ ->3 b))
7	3, 6	wb 1	1 wff (a u3 b) = (a_|_ ->3 (a_|_ ->3 b))

metamath.org