Theorem equequ2 1868

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 1867	. 2 |- ( x = y -> ( x = z <-> y = z ) )
2		equcom 1862	. 2 |- ( x = z <-> z = x )
3		equcom 1862	. 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 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664

This theorem is referenced by:  ax12v  1934  axc11nlem  2021  axc9lem1  2093  axc9lem2  2133  axc9lem2OLD  2134  axc11nlemALT  2142  dveeq2ALT  2174  ax12v2  2175  equvini  2179  sbequi  2204  eujust  2301  eujustALT  2302  euequ1  2305  euf  2307  mo2  2308  disjxun  4400  axrep2  4517  dtru  4594  zfpair  4637  dfid3  4750  isso2i  4787  iotaval  5557  dff13f  6160  dfwe2  6608  aceq0  8549  zfac  8890  axpowndlem4  9025  zfcndac  9044  injresinj  12025  infpn2  14857  ramub1lem2  14985  fullestrcsetc  16036  fullsetcestrc  16051  symgextf1  17062  mplcoe1  18689  evlslem2  18735  mamulid  19466  mamurid  19467  mdetdiagid  19625  dscmet  21587  lgseisenlem2  24278  dchrisumlem3  24329  usgrasscusgra  25211  bj-ssbequ  31242  bj-ssblem1  31243  bj-ssblem2  31244  bj-ssb1a  31245  bj-ssb1  31246  bj-ssbcom3lem  31263  bj-axc11nlemv  31347  bj-axc15v  31362  bj-axrep2  31404  bj-dtru  31412  bj-eleq1w  31455  bj-ax8  31495  wl-aleq  31868  wl-mo2df  31899  wl-eudf  31901  wl-euequ1f  31903  wl-mo2t  31904  wl-ax12v2  31909  wl-ax12v3  31912  dveeq2-o  32504  axc11n-16  32509  ax12eq  32512  ax12inda  32519  ax12v2-o  32520  fphpd  35659  iotavalb  36781