Theorem wr1 197

Description: Weak R1.

Hypothesis

Ref	Expression
wr1.1	(a == b) = 1

Assertion

Ref	Expression
wr1	(b == a) = 1

Proof of Theorem wr1

Step	Hyp	Ref	Expression
1		bicom 96	. 2 (b == a) = (a == b)
2		wr1.1	. 2 (a == b) = 1
3	1, 2	ax-r2 36	1 (b == a) = 1

Syntax hints:   = wb 1   == tb 5  1wt 8

This theorem is referenced by:  wwbmpr 206  wr2 371  w3tr1 374  w3tr2 375  wleoa 376  wleao 377  wom5 381  wcomlem 382  wleror 393  wleran 394  wletr 396  wlbtr 398  wle3tr1 399  wle3tr2 400  wlebi 402  wledi 405  wledio 406  wlecom 409  wcomd 418  wcom3ii 419  wfh1 423  wfh2 424  wfh3 425  wfh4 426  wcom2or 427  wlem14 430  woml6 436  wdid0id5 1108  wdid0id1 1109  wdid0id2 1110  wdid0id3 1111  wdid0id4 1112

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

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

Copyright terms: Public domain