Theorem conb 114

Description: Contraposition law.

Assertion

Ref	Expression
conb	(a ≡ b) = (a⊥ ≡ b⊥ )

Proof of Theorem conb

Step	Hyp	Ref	Expression
1		ax-a2 30	. . 3 ((a ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a ∩ b))
2		ax-a1 29	. . . . 5 a = a⊥ ⊥
3		ax-a1 29	. . . . 5 b = b⊥ ⊥
4	2, 3	2an 72	. . . 4 (a ∩ b) = (a⊥ ⊥ ∩ b⊥ ⊥ )
5	4	lor 66	. . 3 ((a⊥ ∩ b⊥ ) ∪ (a ∩ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ⊥ ∩ b⊥ ⊥ ))
6	1, 5	ax-r2 35	. 2 ((a ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ⊥ ∩ b⊥ ⊥ ))
7		dfb 86	. 2 (a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
8		dfb 86	. 2 (a⊥ ≡ b⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ⊥ ∩ b⊥ ⊥ ))
9	6, 7, 8	3tr1 60	1 (a ≡ b) = (a⊥ ≡ b⊥ )

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

This theorem is referenced by:  di 118  wr4 191  wcon 194  wcon1 199  wcon2 200  wwfh3 210  wwfh4 211  ka4lem 221  ska3 224  nomcon5 298  nom55 328  wom2 416  u3lemax4 778  comanbn 855

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