Theorem equequ2 1736

Description: An equivalence law for equality. (Contributed by NM, 5-Aug-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 1735	. 2 |- ( x = y -> ( x = z <-> y = z ) )
2		equcom 1731	. 2 |- ( x = z <-> z = x )
3		equcom 1731	. 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 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727

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

This theorem is referenced by:  axc9lem1  1944  axc9lem2  1987  axc11nlem  1995  dveeq2ALT  2031  ax12v2  2032  equvini  2036  sbequi  2063  ax12vALT  2133  dveeq2-o  2235  axc11n-16  2240  ax12eq  2243  ax12inda  2250  ax12v2-o  2251  eujust  2256  eujustALT  2257  euf  2261  eufOLD  2262  mo2  2263  moOLD  2300  2mo  2355  2moOLD  2356  2eu6  2363  disjxun  4278  axrep2  4393  dtru  4471  zfpair  4517  dfid3  4624  isso2i  4660  iotaval  5380  dff13f  5960  dfwe2  6382  aceq0  8276  zfac  8617  axpowndlem4  8754  zfcndac  8773  injresinj  11622  infpn2  13956  ramub1lem2  14070  symgextf1  15905  mplcoe1  17477  evlslem2  17524  mamulid  18145  mamurid  18146  dscmet  20006  lgseisenlem2  22573  dchrisumlem3  22624  usgrasscusgra  23213  wl-aleq  28210  wl-mo2dnae  28237  wl-mo2d  28238  fphpd  28997  iotavalb  29526  bj-axc11nlemv  31878  bj-axc15v  31893  bj-axrep2  31927  bj-dtru  31935  bj-eleq1w  31967