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

Theorem equequ1 2032
 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 2023 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2 equtr 2028 . 2 (𝑥 = 𝑦 → (𝑦 = 𝑧𝑥 = 𝑧))
31, 2impbid 215 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782 This theorem is referenced by:  equvinv  2036  equvelv  2038  spaev  2057  sbjust  2068  equsb3  2106  drsb1  2513  mo4  2625  sb8eulem  2659  cbvmow  2663  axextg  2772  cbvabw  2867  reu6  3665  reu7  3671  reu8nf  3806  disjxun  5029  cbviotaw  6293  cbviota  6295  dff13f  6997  poxp  7812  unxpdomlem1  8713  unxpdomlem2  8714  aceq0  9536  zfac  9878  axrepndlem1  10010  zfcndac  10037  injresinj  13160  fsum2dlem  15124  ramub1lem2  16360  ramcl  16362  symgextf1  18549  mamulid  21060  mamurid  21061  mdetdiagid  21219  mdetunilem9  21239  alexsubALTlem3  22668  ptcmplem2  22672  dscmet  23193  dyadmbllem  24217  opnmbllem  24219  isppw2  25714  2sqreulem1  26044  2sqreunnlem1  26047  frgr2wwlk1  28128  disji2f  30354  disjif2  30358  bj-ssblem1  34140  bj-ssblem2  34141  cbveud  34829  wl-naevhba1v  34965  wl-equsb3  34997  mblfinlem1  35134  bfp  35302  dveeq1-o  36271  dveeq1-o16  36272  axc11n-16  36274  ax12eq  36277  fsuppind  39517  mhphf  39523  fphpd  39821  ax6e2nd  41328  ax6e2ndVD  41678  ax6e2ndALT  41700  disjinfi  41883  iundjiun  43160  hspdifhsp  43316  hspmbl  43329  2reu8i  43730  2reuimp0  43731  ichexmpl1  44047  lcoss  44904
 Copyright terms: Public domain W3C validator