Theorem lbi 97

Description: Introduce biconditional to the left. (Contributed by NM, 10-Aug-1997.)

Hypothesis

Ref	Expression
lbi.1	a = b

Assertion

Ref	Expression
lbi	(c ≡ a) = (c ≡ b)

Proof of Theorem lbi

Step	Hyp	Ref	Expression
1		lbi.1	. . . 4 a = b
2	1	lan 77	. . 3 (c ∩ a) = (c ∩ b)
3	1	ax-r4 37	. . . 4 a⊥ = b⊥
4	3	lan 77	. . 3 (c⊥ ∩ a⊥ ) = (c⊥ ∩ b⊥ )
5	2, 4	2or 72	. 2 ((c ∩ a) ∪ (c⊥ ∩ a⊥ )) = ((c ∩ b) ∪ (c⊥ ∩ b⊥ ))
6		dfb 94	. 2 (c ≡ a) = ((c ∩ a) ∪ (c⊥ ∩ a⊥ ))
7		dfb 94	. 2 (c ≡ b) = ((c ∩ b) ∪ (c⊥ ∩ b⊥ ))
8	5, 6, 7	3tr1 63	1 (c ≡ a) = (c ≡ 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-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

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

This theorem is used by:  rbi  98  2bi  99  wcon3  209  wwoml2  212  nom55  336