Theorem equequ2 1693

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 1690	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1690	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1688	. 2 |- ( x = y -> ( z = y -> z = x ) )
4	1, 3	impbid 128	1 |- ( x = y -> ( z = x <-> z = y ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1800  ax11v  1807  ax11ev  1808  equs5or  1810  eujust  2008  euf  2011  mo23  2047  eleq1w  2218  cbvabw  2280  csbcow  3042  disjiun  3962  iotaval  5149  dffun4f  5189  dff13f  5723  supmoti  6940  isoti  6954  exmidontriim  7163  ennnfonelemr  12248  ctinf  12255