Theorem equequ2 1783

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 1782	. 2 |- ( x = y -> ( x = z <-> y = z ) )
2		equcom 1778	. 2 |- ( x = z <-> z = x )
3		equcom 1778	. 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 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774

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

This theorem is referenced by:  ax12v  1839  ax12vOLD  1840  axc11nlem  1922  axc9lem1  1985  axc9lem2  2024  axc11nlemOLD  2032  dveeq2ALT  2066  ax12v2  2067  equvini  2071  sbequi  2100  dveeq2-o  2247  axc11n-16  2252  ax12eq  2255  ax12inda  2262  ax12v2-o  2263  eujust  2268  eujustALT  2269  euequ1  2272  euf  2276  mo2  2277  2eu6OLD  2368  disjxun  4431  axrep2  4546  dtru  4624  zfpair  4670  dfid3  4782  isso2i  4818  iotaval  5548  dff13f  6148  dfwe2  6598  aceq0  8497  zfac  8838  axpowndlem4  8975  zfcndac  8995  injresinj  11900  infpn2  14303  ramub1lem2  14417  symgextf1  16315  mplcoe1  17995  evlslem2  18048  mamulid  18810  mamurid  18811  mdetdiagid  18969  dscmet  20959  lgseisenlem2  23490  dchrisumlem3  23541  usgrasscusgra  24348  wl-aleq  29956  wl-mo2dnae  29987  wl-mo2t  29988  fphpd  30718  iotavalb  31284  bj-axc11nlemv  34027  bj-axc15v  34042  bj-axrep2  34087  bj-dtru  34095  bj-eleq1w  34134