MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equequ2 Structured version   Unicode version

Theorem equequ2 1698
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
StepHypRef Expression
1 equequ1 1696 . 2  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
2 equcom 1692 . 2  |-  ( x  =  z  <->  z  =  x )
3 equcom 1692 . 2  |-  ( y  =  z  <->  z  =  y )
41, 2, 33bitr3g 279 1  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  a9e  1952  ax10lem2  2023  ax10lem2OLD  2026  dveeq2OLD  2029  ax10lem4OLD  2030  ax9OLD  2033  dveeq2  2073  ax11v2  2074  ax11v2OLD  2075  sbequi  2136  ax11vALT  2172  dveeq2-o  2260  dveeq2-o16  2261  ax10-16  2266  ax11eq  2269  ax11inda  2276  ax11v2-o  2277  eujust  2282  eujustALT  2283  euf  2286  mo  2302  2mo  2358  2eu6  2365  disjxun  4202  axrep2  4314  dtru  4382  zfpair  4393  dfid3  4491  isso2i  4527  dfwe2  4754  iotaval  5421  dff13f  5998  aceq0  7989  zfac  8330  axpowndlem4  8465  zfcndac  8484  injresinj  11190  infpn2  13271  ramub1lem2  13385  mplcoe1  16518  evlslem2  16558  dscmet  18610  lgseisenlem2  21124  dchrisumlem3  21175  usgrasscusgra  21482  wl-aleq  26200  fphpd  26831  mamulid  27390  mamurid  27391  iotavalb  27562  dveeq2NEW7  29364  ax9NEW7  29369  ax10lem4NEW7  29372  ax11v2NEW7  29431
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator