Definition df-id3oa 57

Description: The 3-variable orthoarguesian identity term. (Contributed by NM, 22-Sep-1998.)

Assertion

Ref	Expression
df-id3oa	(a ≡ c ≡OA b) = (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))

Detailed syntax breakdown of Definition df-id3oa

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3		wvc	. . 3 term  c
4	1, 2, 3	wid3oa 27	. 2 term  (a ≡ c ≡OA b)
5	1, 3	wi1 12	. . . 4 term  (a →1 c)
6	2, 3	wi1 12	. . . 4 term  (b →1 c)
7	5, 6	wa 7	. . 3 term  ((a →1 c) ∩ (b →1 c))
8	1	wn 4	. . . . 5 term  a⊥
9	8, 3	wi1 12	. . . 4 term  (a⊥ →1 c)
10	2	wn 4	. . . . 5 term  b⊥
11	10, 3	wi1 12	. . . 4 term  (b⊥ →1 c)
12	9, 11	wa 7	. . 3 term  ((a⊥ →1 c) ∩ (b⊥ →1 c))
13	7, 12	wo 6	. 2 term  (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))
14	4, 13	wb 1	1 wff  (a ≡ c ≡OA b) = (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))

This definition is referenced by:  3oa3  1025