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

Theorem equequ1 1998
 Description: An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
Assertion
Ref Expression
equequ1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))

Proof of Theorem equequ1
StepHypRef Expression
1 ax7 1989 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2 equtr 1994 . 2 (𝑥 = 𝑦 → (𝑦 = 𝑧𝑥 = 𝑧))
31, 2impbid 202 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
 Colors of variables: wff setvar class 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 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745 This theorem is referenced by:  spaev  2020  drsb1  2405  equsb3lem  2459  sb8eu  2532  axext3ALT  2634  reu6  3428  reu7  3434  reu8nf  3549  disjxun  4683  cbviota  5894  dff13f  6553  poxp  7334  unxpdomlem1  8205  unxpdomlem2  8206  aceq0  8979  zfac  9320  axrepndlem1  9452  zfcndac  9479  injresinj  12629  fsum2dlem  14545  ramub1lem2  15778  ramcl  15780  symgextf1  17887  mamulid  20295  mamurid  20296  mdetdiagid  20454  mdetunilem9  20474  alexsubALTlem3  21900  ptcmplem2  21904  dscmet  22424  dyadmbllem  23413  opnmbllem  23415  isppw2  24886  frgr2wwlk1  27309  disji2f  29516  disjif2  29520  bj-ssbjust  32743  bj-ssblem1  32755  bj-ssblem2  32756  bj-axext3  32894  wl-naevhba1v  33434  wl-equsb3  33467  mblfinlem1  33576  bfp  33753  dveeq1-o  34539  dveeq1-o16  34540  axc11n-16  34542  ax12eq  34545  fphpd  37697  ax6e2nd  39091  ax6e2ndVD  39458  ax6e2ndALT  39480  disjinfi  39694  iundjiun  40995  hspdifhsp  41151  hspmbl  41164  lcoss  42550
 Copyright terms: Public domain W3C validator