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

Theorem equequ1 1875
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 ax7 1868 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1873 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
31, 2impbid 195 1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672
This theorem is referenced by:  equequ2  1876  spaev  1894  drsb1  2226  equsb3lem  2280  sb8eu  2352  axext3ALT  2454  reu6  3215  reu7  3221  disjxun  4393  cbviota  5558  dff13f  6178  poxp  6927  unxpdomlem1  7794  unxpdomlem2  7795  aceq0  8567  zfac  8908  axrepndlem1  9035  zfcndac  9062  injresinj  12057  fsum2dlem  13908  ramub1lem2  15064  ramcl  15066  symgextf1  17140  mamulid  19543  mamurid  19544  mdetdiagid  19702  mdetunilem9  19722  alexsubALTlem3  21142  ptcmplem2  21146  dscmet  21665  dyadmbllem  22636  opnmbllem  22638  isppw2  24121  frg2wot1  25864  disji2f  28264  disjif2  28268  ghomf1olem  30384  bj-ssblem1  31307  bj-ssblem2  31308  bj-axext3  31450  wl-equsb3  31954  mblfinlem1  32041  bfp  32220  dveeq1-o  32570  dveeq1-o16  32571  axc11n-16  32573  ax12eq  32576  fphpd  35730  ax6e2nd  36995  ax6e2ndVD  37368  ax6e2ndALT  37390  iundjiun  38414  hspdifhsp  38556  hspmbl  38569  lcoss  40737
  Copyright terms: Public domain W3C validator