Theorem wr2 371

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 94	. . . . 5 (b == c) = ((b ^ c) v (b' ^ c'))
3	2	rbi 98	. . . 4 ((b == c) == ((a ^ c) v (b' ^ c'))) = (((b ^ c) v (b' ^ c')) == ((a ^ c) v (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) v (b' ^ c')) == ((a ^ c) v (b' ^ c'))) = 1
8	3, 7	ax-r2 36	. . 3 ((b == c) == ((a ^ c) v (b' ^ c'))) = 1
9	1, 8	wwbmp 205	. 2 ((a ^ c) v (b' ^ c')) = 1
10		dfb 94	. . . 4 (a == c) = ((a ^ c) v (a' ^ c'))
11	10	rbi 98	. . 3 ((a == c) == ((a ^ c) v (b' ^ c'))) = (((a ^ c) v (a' ^ c')) == ((a ^ c) v (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) v (a' ^ c')) == ((a ^ c) v (b' ^ c'))) = 1
15	11, 14	ax-r2 36	. 2 ((a == c) == ((a ^ c) v (b' ^ c'))) = 1
16	9, 15	wwbmpr 206	1 (a == c) = 1

Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8

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 1105  wddi4 1107  wdid0id5 1108  wdid0id1 1109  wdid0id2 1110  wdid0id3 1111  wdid0id4 1112

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

Copyright terms: Public domain