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

Theorem equequ2 1649
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 1648 . 2  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
2 equcom 1647 . 2  |-  ( x  =  z  <->  z  =  x )
3 equcom 1647 . 2  |-  ( y  =  z  <->  z  =  y )
41, 2, 33bitr3g 278 1  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  ax10lem2  1877  dveeq2  1880  ax10lem4  1881  ax9  1889  ax11v2  1932  dveeq2-o  2123  dveeq2-o16  2124  ax10-16  2129  ax11eq  2132  ax11inda  2139  ax11v2-o  2140  eujust  2145  eujustALT  2146  euf  2149  mo  2165  2mo  2221  2eu6  2228  axrep2  4133  dtru  4201  zfpair  4212  dfid3  4310  dfwe2  4573  iotaval  5230  aceq0  7745  zfac  8086  axpowndlem4  8222  zfcndac  8241  infpn2  12960  ramub1lem2  13074  mplcoe1  16209  evlslem2  16249  dscmet  18095  lgseisenlem2  20589  fphpd  26899  mamulid  27458  mamurid  27459  iotavalb  27630  a12stdy2-x12  29112  a12study4  29117  ax10lem17ALT  29123  ax10lem18ALT  29124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator