Theorem equequ2 1134

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 1131	. 2 |- (x = y -> (z = x -> z = y))
2		equtrr 1131	. . 3 |- (y = x -> (z = y -> z = x))
3	2	equcoms 1129	. 2 |- (x = y -> (z = y -> z = x))
4	1, 3	impbid 515	1 |- (x = y -> (z = x <-> z = y))

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

This theorem is referenced by:  dveeq2 1211  dveeq2ALT 1212  ax11v2 1214  sb7f 1340  ax11eq 1362  ax11inda 1370  euf 1383  mo 1392  2mo 1446  2eu6 1453  axrep2 2691  dtruALT 2744  zfpair 2773  dfid3 2832  asymref2 3436  aceq0 4713  axac 4728  axpowndlem4 4935  zfcndac 4954  dscmet 7880

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-8 963  ax-12 967  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122

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

Copyright terms: Public domain