Theorem equequ2 1736

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 1733	. 2 |- ( x = y -> ( z = x -> z = y ) )
2		equtrr 1733	. . 3 |- ( y = x -> ( z = y -> z = x ) )
3	2	equcoms 1731	. 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 1472  ax-ie2 1517  ax-8 1527  ax-17 1549  ax-i9 1553

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1843  ax11v  1850  ax11ev  1851  equs5or  1853  eujust  2056  euf  2059  mo23  2095  eleq1w  2266  cbvabw  2328  csbcow  3104  disjiun  4039  iotaval  5243  dffun4f  5287  dff13f  5839  supmoti  7095  isoti  7109  nninfwlpoim  7281  exmidontriim  7337  netap  7366  ennnfonelemr  12794  ctinf  12801  infpn2  12827  lgseisenlem2  15548