Definition df-a3 54

Description: Defined conjunction.

Assertion

Ref	Expression
df-a3	(a ^3 b) = (a_|_ u3 b_|_)_|_

Detailed syntax breakdown of Definition df-a3

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	wan3 25	. 2 term (a ^3 b)
4	1	wn 4	. . . 4 term a_|_
5	2	wn 4	. . . 4 term b_|_
6	4, 5	wo3 24	. . 3 term (a_|_ u3 b_|_)
7	6	wn 4	. 2 term (a_|_ u3 b_|_)_|_
8	3, 7	wb 1	1 wff (a ^3 b) = (a_|_ u3 b_|_)_|_

metamath.org