Theorem wr1 189

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 88	. 2 (b ≡ a) = (a ≡ b)
2		wr1.1	. 2 (a ≡ b) = 1
3	1, 2	ax-r2 35	1 (b ≡ a) = 1

Syntax hints:   = wb 1   ≡ tb 5  1wt 9

This theorem is referenced by:  wwbmpr 198  wr2 353  w3tr1 356  w3tr2 357  wleoa 358  wleao 359  wom5 363  wcomlem 364  wleror 375  wleran 376  wletr 378  wlbtr 380  wle3tr1 381  wle3tr2 382  wlebi 384  wledi 387  wledio 388  wlecom 391  wcomd 400  wcom3ii 401  wfh1 405  wfh2 406  wfh3 407  wfh4 408  wcom2or 409  wlem14 412  woml6 418

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

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

metamath.org