Definition df-a3 54

Description: Defined conjunction.

Assertion

Ref	Expression
df-a3	(a ∩3 b) = (a⊥ ∪3 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⊥ ∪3 b⊥ )
7	6	wn 4	. 2 term  (a⊥ ∪3 b⊥ )⊥
8	3, 7	wb 1	1 wff  (a ∩3 b) = (a⊥ ∪3 b⊥ )⊥

metamath.org