Theorem bi1 118

Description: Identity inference. (Contributed by NM, 30-Aug-1997.)

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

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