Theorem equequ2 1713

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 1710	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1710	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1708	. 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 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  eujust  2028  euf  2031  mo23  2067  eleq1w  2238  cbvabw  2300  csbcow  3068  disjiun  3998  iotaval  5189  dffun4f  5232  dff13f  5770  supmoti  6991  isoti  7005  nninfwlpoim  7175  exmidontriim  7223  netap  7252  ennnfonelemr  12423  ctinf  12430  infpn2  12456  lgseisenlem2  14421