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

Theorem equequ1 1736
Description: An equivalence law for equality. (Contributed by NM, 1-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-7 1728 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1734 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
31, 2impbid 191 1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
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 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  equequ2  1737  drsb1  2068  equsb3lem  2136  dveeq1-o  2236  dveeq1-o16  2237  axc11n-16  2239  ax12eq  2242  sb8eu  2292  2moOLDOLD  2362  2eu6OLD  2372  euequ1OLD  2375  axext3  2425  reu6  3147  reu7  3153  disjxun  4289  cbviota  5385  dff13f  5972  poxp  6683  unxpdomlem1  7516  unxpdomlem2  7517  aceq0  8287  zfac  8628  axrepndlem1  8755  axpowndlem2OLD  8762  zfcndac  8785  injresinj  11638  fsum2dlem  13236  ramub1lem2  14087  ramcl  14089  symgextf1  15925  mamulid  18303  mamurid  18304  mdetunilem9  18425  alexsubALTlem3  19620  ptcmplem2  19624  dscmet  20164  dyadmbllem  21078  opnmbllem  21080  isppw2  22452  disji2f  25920  disjif2  25924  ghomf1olem  27312  wl-equsb3  28378  bfp  28721  fphpd  29153  frg2wot1  30648  mdetdiagid  30935  lcoss  30968  ax6e2nd  31265  ax6e2ndVD  31642  ax6e2ndALT  31664  bj-axext3  32287
  Copyright terms: Public domain W3C validator