Theorem equequ1 1952

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

Step	Hyp	Ref	Expression
1		ax7 1943	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1948	. 2 |- ( x = y -> ( y = z -> x = z ) )
3	1, 2	impbid 202	1 |- ( x = y -> ( x = z <-> y = z ) )

Syntax hints:   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  equequ2OLD  1955  spaev  1978  drsb1  2377  equsb3lem  2431  sb8eu  2503  axext3ALT  2605  reu6  3395  reu7  3401  reu8nf  3516  disjxun  4651  cbviota  5856  dff13f  6513  poxp  7289  unxpdomlem1  8164  unxpdomlem2  8165  aceq0  8941  zfac  9282  axrepndlem1  9414  zfcndac  9441  injresinj  12589  fsum2dlem  14501  ramub1lem2  15731  ramcl  15733  symgextf1  17841  mamulid  20247  mamurid  20248  mdetdiagid  20406  mdetunilem9  20426  alexsubALTlem3  21853  ptcmplem2  21857  dscmet  22377  dyadmbllem  23367  opnmbllem  23369  isppw2  24841  frgr2wwlk1  27193  disji2f  29390  disjif2  29394  bj-ssbjust  32618  bj-ssblem1  32630  bj-ssblem2  32631  bj-axext3  32769  wl-naevhba1v  33304  wl-equsb3  33337  mblfinlem1  33446  bfp  33623  dveeq1-o  34220  dveeq1-o16  34221  axc11n-16  34223  ax12eq  34226  fphpd  37380  ax6e2nd  38774  ax6e2ndVD  39144  ax6e2ndALT  39166  disjinfi  39380  iundjiun  40677  hspdifhsp  40830  hspmbl  40843  lcoss  42225