Theorem equequ2 1823

Description: An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.)

Assertion

Ref	Expression
equequ2	|- ( x = y -> ( z = x <-> z = y ) )

Proof of Theorem equequ2

Step	Hyp	Ref	Expression
1		equequ1 1822	. 2 |- ( x = y -> ( x = z <-> y = z ) )
2		equcom 1818	. 2 |- ( x = z <-> z = x )
3		equcom 1818	. 2 |- ( y = z <-> z = y )
4	1, 2, 3	3bitr3g 287	1 |- ( x = y -> ( z = x <-> z = y ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814

This theorem depends on definitions:  df-bi 185  df-ex 1634

This theorem is referenced by:  ax12v  1879  ax12vOLD  1880  axc11nlem  1966  axc9lem1  2028  axc9lem2  2066  axc11nlemOLD  2074  dveeq2ALT  2108  ax12v2  2109  equvini  2113  sbequi  2140  eujust  2240  eujustALT  2241  euequ1  2244  euf  2248  mo2  2249  2eu6OLD  2335  disjxun  4393  axrep2  4509  dtru  4585  zfpair  4628  dfid3  4739  isso2i  4776  iotaval  5544  dff13f  6148  dfwe2  6599  aceq0  8531  zfac  8872  axpowndlem4  9007  zfcndac  9027  injresinj  11963  infpn2  14640  ramub1lem2  14754  fullestrcsetc  15744  fullsetcestrc  15759  symgextf1  16770  mplcoe1  18447  evlslem2  18500  mamulid  19235  mamurid  19236  mdetdiagid  19394  dscmet  21385  lgseisenlem2  24006  dchrisumlem3  24057  usgrasscusgra  24900  bj-axc11nlemv  30879  bj-axc15v  30894  bj-axrep2  30939  bj-dtru  30947  bj-eleq1w  30986  wl-aleq  31355  wl-mo2dnae  31386  wl-mo2t  31387  wl-ax12v2  31394  dveeq2-o  31956  axc11n-16  31961  ax12eq  31964  ax12inda  31971  ax12v2-o  31972  fphpd  35111  iotavalb  36185