Theorem equequ2 1137

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 1134	. 2 |- (x = y -> (z = x -> z = y))
2		equtrr 1134	. . 3 |- (y = x -> (z = y -> z = x))
3	2	equcoms 1132	. 2 |- (x = y -> (z = y -> z = x))
4	1, 3	impbid 518	1 |- (x = y -> (z = x <-> z = y))

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

This theorem is referenced by:  dveeq2 1214  dveeq2ALT 1215  ax11v2 1217  sb7f 1343  ax11eq 1365  ax11inda 1373  euf 1386  mo 1395  2mo 1450  2eu6 1457  axrep2 2701  dtruALT 2755  zfpair 2784  dfid3 2843  asymref2 3447  aceq0 4747  axac 4762  axpowndlem4 4971  zfcndac 4990  dscmet 7922

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-8 966  ax-12 970  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125

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

Copyright terms: Public domain