Theorem equequ2 1131

Description: An equivalence law for equality.

Assertion

Ref	Expression
equequ2	|- (x = y -> (z = x <-> z = y))

Proof of Theorem equequ2

Step	Hyp	Ref	Expression
1		equtrr 1128	. 2 |- (x = y -> (z = x -> z = y))
2		equtrr 1128	. . 3 |- (y = x -> (z = y -> z = x))
3	2	equcoms 1126	. 2 |- (x = y -> (z = y -> z = x))
4	1, 3	impbid 514	1 |- (x = y -> (z = x <-> z = y))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953

This theorem is referenced by:  dveeq2 1208  ax11v2 1210  sb7f 1336  ax11eq 1356  ax11inda 1364  euf 1377  mo 1386  2mo 1440  2eu6 1447  axrep2 2685  dtruALT 2738  zfpair 2767  dfid3 2826  asymref2 3424  asymref2OLD 3426  aceq0 4702  axac 4717  axpowndlem4 4924  zfcndac 4943  dscmet 7856

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-8 961  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain