Theorem biao 799

Description: Equivalence to biconditional. (Contributed by NM, 8-Jul-2000.)

Assertion

Ref	Expression
biao	(a ≡ b) = ((a ∩ b) ≡ (a ∪ b))

Proof of Theorem biao

Step	Hyp	Ref	Expression
1		leao1 162	. . . . 5 (a ∩ b) ≤ (a ∪ b)
2	1	df2le2 136	. . . 4 ((a ∩ b) ∩ (a ∪ b)) = (a ∩ b)
3	2	ax-r1 35	. . 3 (a ∩ b) = ((a ∩ b) ∩ (a ∪ b))
4		anor3 90	. . . 4 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
5	1	lecon 154	. . . . . 6 (a ∪ b)⊥ ≤ (a ∩ b)⊥
6		oridm 110	. . . . . . 7 ((a ∪ b)⊥ ∪ (a ∪ b)⊥ ) = (a ∪ b)⊥
7	6	df-le1 130	. . . . . 6 (a ∪ b)⊥ ≤ (a ∪ b)⊥
8	5, 7	ler2an 173	. . . . 5 (a ∪ b)⊥ ≤ ((a ∩ b)⊥ ∩ (a ∪ b)⊥ )
9		lear 161	. . . . . . 7 ((a ∩ b)⊥ ∩ (a ∪ b)⊥ ) ≤ (a ∪ b)⊥
10	9	df-le2 131	. . . . . 6 (((a ∩ b)⊥ ∩ (a ∪ b)⊥ ) ∪ (a ∪ b)⊥ ) = (a ∪ b)⊥
11	10	df-le1 130	. . . . 5 ((a ∩ b)⊥ ∩ (a ∪ b)⊥ ) ≤ (a ∪ b)⊥
12	8, 11	lebi 145	. . . 4 (a ∪ b)⊥ = ((a ∩ b)⊥ ∩ (a ∪ b)⊥ )
13	4, 12	ax-r2 36	. . 3 (a⊥ ∩ b⊥ ) = ((a ∩ b)⊥ ∩ (a ∪ b)⊥ )
14	3, 13	2or 72	. 2 ((a ∩ b) ∪ (a⊥ ∩ b⊥ )) = (((a ∩ b) ∩ (a ∪ b)) ∪ ((a ∩ b)⊥ ∩ (a ∪ b)⊥ ))
15		dfb 94	. 2 (a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
16		dfb 94	. 2 ((a ∩ b) ≡ (a ∪ b)) = (((a ∩ b) ∩ (a ∪ b)) ∪ ((a ∩ b)⊥ ∩ (a ∪ b)⊥ ))
17	14, 15, 16	3tr1 63	1 (a ≡ b) = ((a ∩ b) ≡ (a ∪ b))

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is used by:  mlaconj4  844