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

Theorem equequ2 1693
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 1691 . 2  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
2 equcom 1687 . 2  |-  ( x  =  z  <->  z  =  x )
3 equcom 1687 . 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  1941  dveeq2  1968  ax10lem2OLD  1970  ax10lem4  1973  ax9-OLD  1981  ax11v2  2018  ax11vALT  2123  dveeq2-o  2211  dveeq2-o16  2212  ax10-16  2217  ax11eq  2220  ax11inda  2227  ax11v2-o  2228  eujust  2233  eujustALT  2234  euf  2237  mo  2253  2mo  2309  2eu6  2316  disjxun  4144  axrep2  4256  dtru  4324  zfpair  4335  dfid3  4433  isso2i  4469  dfwe2  4695  iotaval  5362  dff13f  5938  aceq0  7925  zfac  8266  axpowndlem4  8401  zfcndac  8420  injresinj  11120  infpn2  13201  ramub1lem2  13315  mplcoe1  16448  evlslem2  16488  dscmet  18484  lgseisenlem2  20994  dchrisumlem3  21045  usgrasscusgra  21351  fphpd  26561  mamulid  27120  mamurid  27121  iotavalb  27292  dveeq2NEW7  28794  ax9NEW7  28799  ax10lem4NEW7  28802  ax11v2NEW7  28859  a12stdy2-x12  29088  a12study4  29093  ax10lem17ALT  29099  ax10lem18ALT  29100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator