Theorem dfnb 87

Description: Negated biconditional.

Assertion

Ref	Expression
dfnb	(a == b)_|_ = ((a v b) ^ (a_|_ v b_|_))

Proof of Theorem dfnb

Step	Hyp	Ref	Expression
1		oran 79	. . . 4 ((a ^ b) v (a_|_ ^ b_|_)) = ((a ^ b)_|_ ^ (a_|_ ^ b_|_)_|_)_|_
2	1	con2 64	. . 3 ((a ^ b) v (a_|_ ^ b_|_))_|_ = ((a ^ b)_|_ ^ (a_|_ ^ b_|_)_|_)
3		ancom 68	. . 3 ((a ^ b)_|_ ^ (a_|_ ^ b_|_)_|_) = ((a_|_ ^ b_|_)_|_ ^ (a ^ b)_|_)
4	2, 3	ax-r2 35	. 2 ((a ^ b) v (a_|_ ^ b_|_))_|_ = ((a_|_ ^ b_|_)_|_ ^ (a ^ b)_|_)
5		dfb 86	. . 3 (a == b) = ((a ^ b) v (a_|_ ^ b_|_))
6	5	ax-r4 36	. 2 (a == b)_|_ = ((a ^ b) v (a_|_ ^ b_|_))_|_
7		oran 79	. . 3 (a v b) = (a_|_ ^ b_|_)_|_
8		df-a 39	. . . . 5 (a ^ b) = (a_|_ v b_|_)_|_
9	8	con2 64	. . . 4 (a ^ b)_|_ = (a_|_ v b_|_)
10	9	ax-r1 34	. . 3 (a_|_ v b_|_) = (a ^ b)_|_
11	7, 10	2an 72	. 2 ((a v b) ^ (a_|_ v b_|_)) = ((a_|_ ^ b_|_)_|_ ^ (a ^ b)_|_)
12	4, 6, 11	3tr1 60	1 (a == b)_|_ = ((a v b) ^ (a_|_ v b_|_))

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v wo 6   ^ wa 7

This theorem is referenced by:  wnbdi 411  ska2 414  ska4 415  nbdi 468  test2 785

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-b 38  df-a 39

metamath.org