Theorem equequ2 1689

Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem equequ2

Step	Hyp	Ref	Expression
1		equtrr 1686	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1686	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1684	. 2 |- ( x = y -> ( z = y -> z = x ) )
4	1, 3	impbid 128	1 |- ( x = y -> ( z = x <-> z = y ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie2 1470  ax-8 1482  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1792  ax11v  1799  ax11ev  1800  equs5or  1802  eujust  2001  euf  2004  mo23  2040  eleq1w  2200  disjiun  3924  iotaval  5099  dffun4f  5139  dff13f  5671  supmoti  6880  isoti  6894  ennnfonelemr  11936  ctinf  11943