Definition df-b3 55

Description: Defined biconditional.

Assertion

Ref	Expression
df-b3	(a ↔3 b) = ((a →3 b) ∩ (b →3 a))

Detailed syntax breakdown of Definition df-b3

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wb3 23	. 2 term  (a ↔3 b)
4	1, 2	wi3 15	. . 3 term  (a →3 b)
5	2, 1	wi3 15	. . 3 term  (b →3 a)
6	4, 5	wa 7	. 2 term  ((a →3 b) ∩ (b →3 a))
7	3, 6	wb 1	1 wff  (a ↔3 b) = ((a →3 b) ∩ (b →3 a))

metamath.org