Theorem wr2 371

Description: Inference rule of AUQL. (Contributed by NM, 24-Sep-1997.)

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 94	. . . . 5 (b ≡ c) = ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))
3	2	rbi 98	. . . 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 197	. . . . . 6 (b ≡ a) = 1
6	5	wran 369	. . . . 5 ((b ∩ c) ≡ (a ∩ c)) = 1
7	6	wr5-2v 366	. . . 4 (((b ∩ c) ∪ (b⊥ ∩ c⊥ )) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = 1
8	3, 7	ax-r2 36	. . 3 ((b ≡ c) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = 1
9	1, 8	wwbmp 205	. 2 ((a ∩ c) ∪ (b⊥ ∩ c⊥ )) = 1
10		dfb 94	. . . 4 (a ≡ c) = ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))
11	10	rbi 98	. . 3 ((a ≡ c) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ )))
12	4	wr4 199	. . . . 5 (a⊥ ≡ b⊥ ) = 1
13	12	wran 369	. . . 4 ((a⊥ ∩ c⊥ ) ≡ (b⊥ ∩ c⊥ )) = 1
14	13	wlor 368	. . 3 (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = 1
15	11, 14	ax-r2 36	. 2 ((a ≡ c) ≡ ((a ∩ c) ∪ (b⊥ ∩ c⊥ ))) = 1
16	9, 15	wwbmpr 206	1 (a ≡ c) = 1

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

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le1 130  df-le2 131

This theorem is referenced by:  w2or  372  w2an  373  w3tr1  374  wleoa  376  wleao  377  wom5  381  wcomlem  382  wdf-c1  383  wlea  388  wlel  392  wleror  393  wleran  394  wletr  396  wbltr  397  wlbtr  398  wbile  401  wlebi  402  wlecom  409  wcbtr  411  wcomcom2  415  wcomd  418  wcom3ii  419  wcomdr  421  wcom3i  422  wfh1  423  wfh2  424  wfh3  425  wfh4  426  wcom2or  427  wnbdi  429  ska2  432  woml6  436  woml7  437  wddi2  1108  wddi4  1110  wdid0id5  1111  wdid0id1  1112  wdid0id2  1113  wdid0id3  1114  wdid0id4  1115