Theorem equequ2 1876

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 1875	. 2 |- ( x = y -> ( x = z <-> y = z ) )
2		equcom 1870	. 2 |- ( x = z <-> z = x )
3		equcom 1870	. 2 |- ( y = z <-> z = y )
4	1, 2, 3	3bitr3g 295	1 |- ( x = y -> ( z = x <-> z = y ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672

This theorem is referenced by:  aevlem0  1896  axc11nlemOLD2  1902  ax12vOLDOLD  1954  axc11nlemOLD  2041  axc9lem1  2106  axc9lem2  2146  axc9lem2OLD  2147  axc15  2153  axc11nlemALT  2156  dveeq2ALT  2189  ax12v2OLD  2191  equvini  2195  sbequi  2224  eujust  2321  eujustALT  2322  euequ1  2325  euf  2327  mo2  2328  disjxun  4393  axrep2  4510  dtru  4592  zfpair  4637  dfid3  4755  isso2i  4792  iotaval  5564  dff13f  6178  dfwe2  6627  aceq0  8567  zfac  8908  axpowndlem4  9043  zfcndac  9062  injresinj  12057  infpn2  14936  ramub1lem2  15064  fullestrcsetc  16114  fullsetcestrc  16129  symgextf1  17140  mplcoe1  18766  evlslem2  18812  mamulid  19543  mamurid  19544  mdetdiagid  19702  dscmet  21665  lgseisenlem2  24357  dchrisumlem3  24408  usgrasscusgra  25290  bj-ssbequ  31306  bj-ssblem1  31307  bj-ssblem2  31308  bj-ssb1a  31309  bj-ssb1  31310  bj-ssbcom3lem  31327  bj-axc11nlemv  31413  bj-axc15v  31428  bj-axrep2  31470  bj-dtru  31478  bj-eleq1w  31523  bj-ax8  31563  wl-aleq  31938  wl-mo2df  31969  wl-eudf  31971  wl-euequ1f  31973  wl-mo2t  31974  dveeq2-o  32568  axc11n-16  32573  ax12eq  32576  ax12inda  32583  ax12v2-o  32584  fphpd  35730  iotavalb  36851