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

Theorem equequ2 1669
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 1667 . 2  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
2 equcom 1665 . 2  |-  ( x  =  z  <->  z  =  x )
3 equcom 1665 . 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  1890  dveeq2  1893  ax10lem4  1894  ax9  1902  ax11v2  1945  dveeq2-o  2136  dveeq2-o16  2137  ax10-16  2142  ax11eq  2145  ax11inda  2152  ax11v2-o  2153  eujust  2158  eujustALT  2159  euf  2162  mo  2178  2mo  2234  2eu6  2241  axrep2  4149  dtru  4217  zfpair  4228  dfid3  4326  dfwe2  4589  iotaval  5246  aceq0  7761  zfac  8102  axpowndlem4  8238  zfcndac  8257  infpn2  12976  ramub1lem2  13090  mplcoe1  16225  evlslem2  16265  dscmet  18111  lgseisenlem2  20605  fphpd  27002  mamulid  27561  mamurid  27562  iotavalb  27733  injresinj  28215  dveeq2NEW7  29440  ax9NEW7  29445  ax10lem4NEW7  29448  ax11v2NEW7  29505  a12stdy2-x12  29734  a12study4  29739  ax10lem17ALT  29745  ax10lem18ALT  29746
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator