Theorem dfb 94

Description: Biconditional expressed with others.

Assertion

Ref	Expression
dfb	(a == b) = ((a ^ b) v (a' ^ b'))

Proof of Theorem dfb

Step	Hyp	Ref	Expression
1		df-b 39	. 2 (a == b) = ((a' v b')' v (a v b)')
2		df-a 40	. . . 4 (a ^ b) = (a' v b')'
3	2	ax-r1 35	. . 3 (a' v b')' = (a ^ b)
4		oran 87	. . . 4 (a v b) = (a' ^ b')'
5	4	con2 67	. . 3 (a v b)' = (a' ^ b')
6	3, 5	2or 72	. 2 ((a' v b')' v (a v b)') = ((a ^ b) v (a' ^ b'))
7	1, 6	ax-r2 36	1 (a == b) = ((a ^ b) v (a' ^ b'))

Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7

This theorem is referenced by:  dfnb 95  bicom 96  lbi 97  biid 116  1b 117  conb 122  mi 125  wlem3.1 210  ka4lemo 228  ska13 241  wlem1 243  nom25 318  id5leid0 351  2vwomlem 365  wr2 371  wdf-c2 384  ska2 432  ska4 433  woml7 437  combi 485  oml4 487  i3bi 496  u1lembi 720  u2lembi 721  i2bi 722  u4lembi 724  u5lembi 725  u12lembi 726  u21lembi 727  bi1o1a 798  biao 799  mlalem 832  bi3 839  orbi 842  mlaconj4 844  comanblem2 871  mlaconjo 886  oa3-3lem 981  oa3-4lem 983  mloa 1018  wdcom 1102  wdid0id5 1108

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

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

Copyright terms: Public domain