Theorem bicom 88

Description: Commutative law.

Assertion

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

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		ancom 68	. . 3 (a ∩ b) = (b ∩ a)
2		ancom 68	. . 3 (a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ )
3	1, 2	2or 67	. 2 ((a ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((b ∩ a) ∪ (b⊥ ∩ a⊥ ))
4		dfb 86	. 2 (a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
5		dfb 86	. 2 (b ≡ a) = ((b ∩ a) ∪ (b⊥ ∩ a⊥ ))
6	3, 4, 5	3tr1 60	1 (a ≡ b) = (b ≡ a)

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7

This theorem is referenced by:  rbi 90  wr1 189  wwfh1 208  wwfh2 209  ska12 232  nomcon5 298  nom35 316  nom55 328  nom65 334  wr5 413  ka4ot 417  ublemc2 711  mlaconj4 826  distid 869  oago3.29 871  oago3.21x 872

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