Theorem equequ2 1748

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 1747	. 2 |- ( x = y -> ( x = z <-> y = z ) )
2		equcom 1743	. 2 |- ( x = z <-> z = x )
3		equcom 1743	. 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 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739

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

This theorem is referenced by:  ax12v  1804  ax12vOLD  1805  axc11nlem  1885  axc9lem1  1970  axc9lem2  2013  axc11nlemOLD  2021  dveeq2ALT  2055  ax12v2  2056  equvini  2060  sbequi  2089  dveeq2-o  2256  axc11n-16  2261  ax12eq  2264  ax12inda  2271  ax12v2-o  2272  eujust  2277  eujustALT  2278  euequ1  2281  euf  2285  eufOLD  2286  mo2  2287  moOLD  2327  2moOLDOLD  2384  2eu6OLD  2394  disjxun  4445  axrep2  4560  dtru  4638  zfpair  4684  dfid3  4796  isso2i  4832  iotaval  5562  dff13f  6156  dfwe2  6602  aceq0  8500  zfac  8841  axpowndlem4  8978  zfcndac  8998  injresinj  11895  infpn2  14293  ramub1lem2  14407  symgextf1  16260  mplcoe1  17938  evlslem2  17991  mamulid  18750  mamurid  18751  mdetdiagid  18909  dscmet  20920  lgseisenlem2  23450  dchrisumlem3  23501  usgrasscusgra  24256  wl-aleq  29841  wl-mo2dnae  29872  wl-mo2t  29873  fphpd  30581  iotavalb  31142  bj-axc11nlemv  33613  bj-axc15v  33628  bj-axrep2  33673  bj-dtru  33681  bj-eleq1w  33720