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

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
StepHypRef 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 )
41, 2, 33bitr3g 287 1  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator