Theorem equequ2 1737

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 1736	. 2 |- ( x = y -> ( x = z <-> y = z ) )
2		equcom 1732	. 2 |- ( x = z <-> z = x )
3		equcom 1732	. 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 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728

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

This theorem is referenced by:  axc9lem1  1945  axc9lem2  1988  axc11nlem  1996  dveeq2ALT  2032  ax12v2  2033  equvini  2037  sbequi  2066  ax12vALT  2131  dveeq2-o  2234  axc11n-16  2239  ax12eq  2242  ax12inda  2249  ax12v2-o  2250  eujust  2255  eujustALT  2256  euequ1  2259  euf  2263  eufOLD  2264  mo2  2265  moOLD  2305  2moOLDOLD  2362  2eu6OLD  2372  disjxun  4311  axrep2  4426  dtru  4504  zfpair  4550  dfid3  4658  isso2i  4694  iotaval  5413  dff13f  5994  dfwe2  6414  aceq0  8309  zfac  8650  axpowndlem4  8787  zfcndac  8807  injresinj  11660  infpn2  13995  ramub1lem2  14109  symgextf1  15947  mplcoe1  17566  evlslem2  17619  mamulid  18326  mamurid  18327  dscmet  20187  lgseisenlem2  22711  dchrisumlem3  22762  usgrasscusgra  23413  wl-aleq  28390  wl-mo2dnae  28421  wl-mo2t  28422  fphpd  29181  iotavalb  29710  mdetdiagid  30934  bj-axc11nlemv  32346  bj-axc15v  32361  bj-axrep2  32406  bj-dtru  32414  bj-eleq1w  32453