Theorem equequ2 1727

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 1724	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1724	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1722	. 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 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1834  ax11v  1841  ax11ev  1842  equs5or  1844  eujust  2047  euf  2050  mo23  2086  eleq1w  2257  cbvabw  2319  csbcow  3095  disjiun  4029  iotaval  5231  dffun4f  5275  dff13f  5820  supmoti  7068  isoti  7082  nninfwlpoim  7253  exmidontriim  7308  netap  7337  ennnfonelemr  12665  ctinf  12672  infpn2  12698  lgseisenlem2  15396