Theorem bi1 110

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 90	. 2 (a ≡ b) = (b ≡ b)
3		biid 108	. 2 (b ≡ b) = 1
4	2, 3	ax-r2 35	1 (a ≡ b) = 1

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

This theorem is referenced by:  1bi 111  wa1 183  wa2 184  wa3 185  wa4 186  wa5 187  wa6 188  wa5b 192  wa5c 193  wcon 194  wancom 195  wanass 196  ska2a 218  ska2b 219  ska5 225  ska6 226  ska7 227  ska8 228  ska9 229  ska10 230  ska12 232  bina1 274  bina2 275  wom5 363  wcomlem 364  wdf-c1 365  wle1 371  wle0 372  wlel 374  wleror 375  wleran 376  wlecon 377  wletr 378  wbile 383  wlebi 384  wle2or 385  wle2an 386  wledi 387  wledio 388  wcom0 389  wcom1 390  wlecom 391  wcomcom2 397  wcomd 400  wcom3ii 401  wcomcom5 402  wcomdr 403  wcom3i 404  wfh1 405  wfh2 406  wfh3 407  wfh4 408  wcom2or 409  wcom2an 410  wnbdi 411  wlem14 412  ska2 414  ska4 415  woml6 418  woml7 419  i3aa 503  i3abs2 505  i3orcom 507  i3ancom 508  bi3tr 509  i3btr 510  i3th6 530

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

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

metamath.org