Theorem equequ2 1690

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 1687	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1687	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1685	. 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 1426  ax-ie2 1471  ax-8 1483  ax-17 1507  ax-i9 1511

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1793  ax11v  1800  ax11ev  1801  equs5or  1803  eujust  2002  euf  2005  mo23  2041  eleq1w  2201  disjiun  3932  iotaval  5107  dffun4f  5147  dff13f  5679  supmoti  6888  isoti  6902  ennnfonelemr  11972  ctinf  11979