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

Theorem equequ1 1852
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 1843 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1850 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
31, 2impbid 193 1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843
This theorem depends on definitions:  df-bi 188  df-ex 1658
This theorem is referenced by:  equequ2  1853  drsb1  2182  equsb3lem  2237  sb8eu  2309  axext3OLD  2411  reu6  3202  reu7  3208  disjxun  4364  cbviota  5513  dff13f  6119  poxp  6863  unxpdomlem1  7729  unxpdomlem2  7730  aceq0  8500  zfac  8841  axrepndlem1  8968  zfcndac  8995  injresinj  11975  fsum2dlem  13774  ramub1lem2  14928  ramcl  14930  symgextf1  17005  mamulid  19408  mamurid  19409  mdetdiagid  19567  mdetunilem9  19587  alexsubALTlem3  21006  ptcmplem2  21010  dscmet  21529  dyadmbllem  22499  opnmbllem  22501  isppw2  23984  frg2wot1  25727  disji2f  28133  disjif2  28137  ghomf1olem  30264  bj-axext3  31294  wl-equsb3  31791  mblfinlem1  31884  bfp  32063  dveeq1-o  32418  dveeq1-o16  32419  axc11n-16  32421  ax12eq  32424  fphpd  35571  ax6e2nd  36838  ax6e2ndVD  37221  ax6e2ndALT  37243  iundjiun  38149  lcoss  39822
  Copyright terms: Public domain W3C validator