Definition df-b 39

Description: Define biconditional.

Assertion

Ref	Expression
df-b	(a == b) = ((a' v b')' v (a v b)')

Detailed syntax breakdown of Definition df-b

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	tb 5	. 2 term (a == b)
4	1	wn 4	. . . . 5 term a'
5	2	wn 4	. . . . 5 term b'
6	4, 5	wo 6	. . . 4 term (a' v b')
7	6	wn 4	. . 3 term (a' v b')'
8	1, 2	wo 6	. . . 4 term (a v b)
9	8	wn 4	. . 3 term (a v b)'
10	7, 9	wo 6	. 2 term ((a' v b')' v (a v b)')
11	3, 10	wb 1	1 wff (a == b) = ((a' v b')' v (a v b)')

This definition is referenced by:  dfb 88  wa6 190  r3a 426

Copyright terms: Public domain