Theorem equequ2 1759

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 1756	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1756	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1754	. 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 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  eujust  2079  euf  2082  mo23  2119  eleq1w  2290  cbvabw  2352  csbcow  3135  disjiun  4078  iotaval  5290  dffun4f  5334  dff13f  5894  supmoti  7160  isoti  7174  nninfwlpoim  7346  exmidontriim  7407  netap  7440  ennnfonelemr  12994  ctinf  13001  infpn2  13027  lgseisenlem2  15750