Theorem equequ2 1724

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 1721	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1721	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1719	. 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 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1831  ax11v  1838  ax11ev  1839  equs5or  1841  eujust  2044  euf  2047  mo23  2083  eleq1w  2254  cbvabw  2316  csbcow  3092  disjiun  4025  iotaval  5227  dffun4f  5271  dff13f  5814  supmoti  7054  isoti  7068  nninfwlpoim  7239  exmidontriim  7287  netap  7316  ennnfonelemr  12583  ctinf  12590  infpn2  12616  lgseisenlem2  15228