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

Theorem equequ1 1648
Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
equequ1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )

Proof of Theorem equequ1
StepHypRef Expression
1 ax-8 1643 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equcomi 1646 . . 3  |-  ( x  =  y  ->  y  =  x )
3 ax-8 1643 . . 3  |-  ( y  =  x  ->  (
y  =  z  ->  x  =  z )
)
42, 3syl 15 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
51, 4impbid 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  1649  ax12olem6  1873  ax10lem2  1877  ax10lem4  1881  equveli  1928  dveeq1  1958  drsb1  1962  equsb3lem  2040  dveeq1-o  2126  dveeq1-o16  2127  ax10-16  2129  ax11eq  2132  2mo  2221  2eu6  2228  euequ1  2231  axext3  2266  cbviota  5224  poxp  6227  unxpdomlem1  7067  unxpdomlem2  7068  aceq0  7745  zfac  8086  axrepndlem1  8214  axpowndlem2  8220  zfcndac  8241  fsum2dlem  12233  ramub1lem2  13074  ramcl  13076  alexsubALTlem3  17743  ptcmplem2  17747  dscmet  18095  isppw2  20353  ghomf1olem  24001  dffix2  24445  bfp  26548  fphpd  26899  mamulid  27458  mamurid  27459  a9e2nd  28324  a9e2ndVD  28684  a9e2ndALT  28707  equvinv  29114  equveliv  29115  a12study4  29117  a12lem1  29130  a12study2  29134  a12study10  29136  a12study10n  29137
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator