Theorem bi1 118

Description: Identity inference.

Hypothesis

Ref	Expression
bi1.1	a = b

Assertion

Ref	Expression
bi1	(a == b) = 1

Proof of Theorem bi1

Step	Hyp	Ref	Expression
1		bi1.1	. . 3 a = b
2	1	rbi 98	. 2 (a == b) = (b == b)
3		biid 116	. 2 (b == b) = 1
4	2, 3	ax-r2 36	1 (a == b) = 1

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

This theorem is referenced by:  1bi 119  wa1 191  wa2 192  wa3 193  wa4 194  wa5 195  wa6 196  wa5b 200  wa5c 201  wcon 202  wancom 203  wanass 204  ska2a 226  ska2b 227  ska5 233  ska6 234  ska7 235  ska8 236  ska9 237  ska10 238  ska12 240  bina1 282  bina2 283  wom5 381  wcomlem 382  wdf-c1 383  wle1 389  wle0 390  wlel 392  wleror 393  wleran 394  wlecon 395  wletr 396  wbile 401  wlebi 402  wle2or 403  wle2an 404  wledi 405  wledio 406  wcom0 407  wcom1 408  wlecom 409  wcomcom2 415  wcomd 418  wcom3ii 419  wcomcom5 420  wcomdr 421  wcom3i 422  wfh1 423  wfh2 424  wfh3 425  wfh4 426  wcom2or 427  wcom2an 428  wnbdi 429  wlem14 430  ska2 432  ska4 433  woml6 436  woml7 437  i3aa 521  i3abs2 523  i3orcom 525  i3ancom 526  bi3tr 527  i3btr 528  i3th6 548

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  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