Theorem equequ2 1850

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 1849	. 2 |- ( x = y -> ( x = z <-> y = z ) )
2		equcom 1845	. 2 |- ( x = z <-> z = x )
3		equcom 1845	. 2 |- ( y = z <-> z = y )
4	1, 2, 3	3bitr3g 291	1 |- ( x = y -> ( z = x <-> z = y ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840

This theorem depends on definitions:  df-bi 189  df-ex 1661

This theorem is referenced by:  ax12v  1907  ax12vOLD  1908  axc11nlem  1995  axc9lem1  2056  axc9lem2  2095  axc9lem2OLD  2096  axc11nlemOLD  2104  dveeq2ALT  2138  ax12v2  2139  equvini  2143  sbequi  2170  eujust  2268  eujustALT  2269  euequ1  2272  euf  2275  mo2  2276  disjxun  4419  axrep2  4536  dtru  4613  zfpair  4656  dfid3  4767  isso2i  4804  iotaval  5574  dff13f  6173  dfwe2  6620  aceq0  8551  zfac  8892  axpowndlem4  9027  zfcndac  9046  injresinj  12026  infpn2  14850  ramub1lem2  14978  fullestrcsetc  16029  fullsetcestrc  16044  symgextf1  17055  mplcoe1  18682  evlslem2  18728  mamulid  19458  mamurid  19459  mdetdiagid  19617  dscmet  21579  lgseisenlem2  24270  dchrisumlem3  24321  usgrasscusgra  25203  bj-axc11nlemv  31308  bj-axc15v  31323  bj-axrep2  31368  bj-dtru  31376  bj-eleq1w  31419  bj-ax8  31458  wl-aleq  31826  wl-mo2df  31857  wl-eudf  31859  wl-euequ1f  31861  wl-mo2t  31862  wl-ax12v2  31867  wl-ax12v3  31870  dveeq2-o  32467  axc11n-16  32472  ax12eq  32475  ax12inda  32482  ax12v2-o  32483  fphpd  35622  iotavalb  36683