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

Theorem equequ1 1697
Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
Assertion
Ref Expression
equequ1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )

Proof of Theorem equequ1
StepHypRef Expression
1 ax-8 1688 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1695 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
31, 2impbid 185 1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  equequ2  1699  ax12olem6OLD  2017  ax10lem2OLD  2027  ax10lem4OLD  2031  dveeq1OLD  2077  equveliOLD  2087  drsb1  2114  equsb3lem  2179  dveeq1-o  2266  dveeq1-o16  2267  ax10-16  2269  ax11eq  2272  2mo  2361  2eu6  2368  euequ1  2371  axext3  2421  reu6  3125  reu7  3131  disjxun  4212  cbviota  5425  dff13f  6008  poxp  6460  unxpdomlem1  7315  unxpdomlem2  7316  aceq0  8001  zfac  8342  axrepndlem1  8469  axpowndlem2  8475  zfcndac  8496  injresinj  11202  fsum2dlem  12556  ramub1lem2  13397  ramcl  13399  alexsubALTlem3  18082  ptcmplem2  18086  dscmet  18622  dyadmbllem  19493  opnmbllem  19495  isppw2  20900  disji2f  24021  disjif2  24025  ghomf1olem  25107  bfp  26535  fphpd  26879  mamulid  27437  mamurid  27438  frg2wot1  28508  a9e2nd  28707  a9e2ndVD  29082  a9e2ndALT  29104  ax12olem6NEW7  29521  dveeq1NEW7  29526  drsb1NEW7  29568  equveliNEW7  29590  equsb3lemNEW7  29663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator