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

Theorem equequ1 2028
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 2019 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2 equtr 2024 . 2 (𝑥 = 𝑦 → (𝑦 = 𝑧𝑥 = 𝑧))
31, 2impbid 211 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 1913  ax-6 1971  ax-7 2011
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782
This theorem is referenced by:  equvinv  2032  equvelv  2034  spaev  2055  sbjust  2066  equsb3  2101  sbievg  2360  drsb1  2498  mo4  2565  sb8eulem  2597  cbvmovw  2601  cbvmow  2602  axextg  2710  reu6  3682  reu7  3688  reu8nf  3831  disjxun  5101  solin  5568  cbviotaw  6452  cbviota  6455  dff13f  7199  poxp  8052  poxp2  8067  poxp3  8074  unxpdomlem1  9152  unxpdomlem2  9153  aceq0  10012  zfac  10354  axrepndlem1  10486  zfcndac  10513  injresinj  13647  fsum2dlem  15615  ramub1lem2  16859  ramcl  16861  symgextf1  19162  mamulid  21742  mamurid  21743  mdetdiagid  21901  mdetunilem9  21921  alexsubALTlem3  23352  ptcmplem2  23356  dscmet  23880  dyadmbllem  24915  opnmbllem  24917  isppw2  26416  2sqreulem1  26746  2sqreunnlem1  26749  frgr2wwlk1  29102  disji2f  31324  disjif2  31328  bj-ssblem1  35056  bj-ssblem2  35057  cbveud  35781  wl-naevhba1v  35917  wl-equsb3  35949  mblfinlem1  36053  bfp  36221  dveeq1-o  37335  dveeq1-o16  37336  axc11n-16  37338  ax12eq  37341  fsuppind  40674  mhphf  40680  fphpd  41048  ax6e2nd  42751  ax6e2ndVD  43101  ax6e2ndALT  43123  disjinfi  43317  iundjiun  44602  hspdifhsp  44758  hspmbl  44771  2reu8i  45246  2reuimp0  45247  ichexmpl1  45562  lcoss  46418
  Copyright terms: Public domain W3C validator