Theorem equequ2 1737

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 1734	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1734	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1732	. 2 |- ( x = y -> ( z = y -> z = x ) )
4	1, 3	impbid 129	1 |- ( x = y -> ( z = x <-> z = y ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1844  ax11v  1851  ax11ev  1852  equs5or  1854  eujust  2057  euf  2060  mo23  2097  eleq1w  2268  cbvabw  2330  csbcow  3112  disjiun  4054  iotaval  5262  dffun4f  5306  dff13f  5862  supmoti  7121  isoti  7135  nninfwlpoim  7307  exmidontriim  7368  netap  7401  ennnfonelemr  12909  ctinf  12916  infpn2  12942  lgseisenlem2  15663