Theorem wr1 197

Description: Weak R1. (Contributed by NM, 2-Sep-1997.)

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 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

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  1111  wdid0id1  1112  wdid0id2  1113  wdid0id3  1114  wdid0id4  1115