Theorem bicom 96

Description: Commutative law.

Assertion

Ref	Expression
bicom	(a == b) = (b == a)

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		ancom 74	. . 3 (a ^ b) = (b ^ a)
2		ancom 74	. . 3 (a' ^ b') = (b' ^ a')
3	1, 2	2or 72	. 2 ((a ^ b) v (a' ^ b')) = ((b ^ a) v (b' ^ a'))
4		dfb 94	. 2 (a == b) = ((a ^ b) v (a' ^ b'))
5		dfb 94	. 2 (b == a) = ((b ^ a) v (b' ^ a'))
6	3, 4, 5	3tr1 63	1 (a == b) = (b == a)

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

This theorem is referenced by:  rbi 98  wr1 197  wwfh1 216  wwfh2 217  ska12 240  nomcon5 306  nom35 324  nom55 336  nom65 342  ka4ot 435  ublemc2 729  mlaconj4 844  distid 887  oago3.29 889  oago3.21x 890

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