Theorem equequ2 1765

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  eujust  2088  euf  2091  mo23  2128  eleq1w  2299  cbvabw  2363  csbcow  3158  disjiun  4125  iotaval  5349  dffun4f  5393  dff13f  5976  modom  7108  supmoti  7334  isoti  7348  nninfwlpoim  7520  exmidontriim  7582  netap  7621  ennnfonelemr  13366  ctinf  13373  infpn2  13399  lgseisenlem2  16356