Theorem wr2 353

Description: Inference rule of AUQL.

Hypotheses

Ref	Expression
wr2.1	(a ≡ b) = 1
wr2.2	(b ≡ c) = 1

Assertion

Ref	Expression
wr2	(a ≡ c) = 1

Proof of Theorem wr2

Step	Hyp	Ref	Expression
1		wr2.2	. . 3 (b ≡ c) = 1
2		dfb 86	. . . . 5 (b ≡ c) = ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))
3	2	rbi 90	. . . 4 ((b ≡ c) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = (((b ∩ c) ∪ (b⊥ ∩ c⊥ )) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ )))
4		wr2.1	. . . . . . 7 (a ≡ b) = 1
5	4	wr1 189	. . . . . 6 (b ≡ a) = 1
6	5	wran 351	. . . . 5 ((b ∩ c) ≡ (a ∩ c)) = 1
7	6	wr5-2v 348	. . . 4 (((b ∩ c) ∪ (b⊥ ∩ c⊥ )) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = 1
8	3, 7	ax-r2 35	. . 3 ((b ≡ c) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = 1
9	1, 8	wwbmp 197	. 2 ((a ∩ c) ∪ (b⊥ ∩ c⊥ )) = 1
10		dfb 86	. . . 4 (a ≡ c) = ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))
11	10	rbi 90	. . 3 ((a ≡ c) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ )))
12	4	wr4 191	. . . . 5 (a⊥ ≡ b⊥ ) = 1
13	12	wran 351	. . . 4 ((a⊥ ∩ c⊥ ) ≡ (b⊥ ∩ c⊥ )) = 1
14	13	wlor 350	. . 3 (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = 1
15	11, 14	ax-r2 35	. 2 ((a ≡ c) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = 1
16	9, 15	wwbmpr 198	1 (a ≡ c) = 1

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

This theorem is referenced by:  w2or 354  w2an 355  w3tr1 356  wleoa 358  wleao 359  wom5 363  wcomlem 364  wdf-c1 365  wlea 370  wlel 374  wleror 375  wleran 376  wletr 378  wbltr 379  wlbtr 380  wbile 383  wlebi 384  wlecom 391  wcbtr 393  wcomcom2 397  wcomd 400  wcom3ii 401  wcomdr 403  wcom3i 404  wfh1 405  wfh2 406  wfh3 407  wfh4 408  wcom2or 409  wnbdi 411  ska2 414  woml6 418  woml7 419

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-wom 343

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le1 122  df-le2 123

metamath.org