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

Theorem equequ1 1675
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 1666 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1673 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
31, 2impbid 183 1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  equequ2  1677  ax12olem6  1904  ax10lem2  1909  ax10lem4  1913  equveli  1960  dveeq1  1990  drsb1  1994  equsb3lem  2073  dveeq1-o  2159  dveeq1-o16  2160  ax10-16  2162  ax11eq  2165  2mo  2254  2eu6  2261  euequ1  2264  axext3  2299  cbviota  5261  poxp  6269  unxpdomlem1  7110  unxpdomlem2  7111  aceq0  7790  zfac  8131  axrepndlem1  8259  axpowndlem2  8265  zfcndac  8286  fsum2dlem  12280  ramub1lem2  13121  ramcl  13123  alexsubALTlem3  17795  ptcmplem2  17799  dscmet  18147  isppw2  20406  ghomf1olem  24285  dffix2  24830  bfp  25696  fphpd  26047  mamulid  26606  mamurid  26607  injresinj  27277  a9e2nd  27818  a9e2ndVD  28195  a9e2ndALT  28218  ax12olem6NEW7  28631  dveeq1NEW7  28636  ax10lem4NEW7  28643  drsb1NEW7  28678  equveliNEW7  28698  equsb3lemNEW7  28768  equvinv  28932  equveliv  28933  a12study4  28935  a12lem1  28948  a12study2  28952  a12study10  28954  a12study10n  28955
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666
This theorem depends on definitions:  df-bi 177  df-ex 1533
  Copyright terms: Public domain W3C validator