Theorem wwbmp 205

Description: Weak weak equivalential detachment (WBMP).

Hypotheses

Ref	Expression
wwbmp.1	a = 1
wwbmp.2	(a == b) = 1

Assertion

Ref	Expression
wwbmp	b = 1

Proof of Theorem wwbmp

Step	Hyp	Ref	Expression
1		wwbmp.1	. . . . 5 a = 1
2	1	rbi 98	. . . 4 (a == b) = (1 == b)
3	2	ax-r1 35	. . 3 (1 == b) = (a == b)
4		wwbmp.2	. . 3 (a == b) = 1
5	3, 4	ax-r2 36	. 2 (1 == b) = 1
6	5	wr3 198	1 b = 1

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

This theorem is referenced by:  wwbmpr 206  bina1 282  bina2 283  wr2 371  ska2 432  i3abs2 523  i3orcom 525  i3ancom 526  i3btr 528  wdid0id5 1108  wdid0id1 1109  wdid0id2 1110  wdid0id3 1111  wdid0id4 1112

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42

Copyright terms: Public domain