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

Theorem equequ2 1999
Description: An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof shortened by BJ, 12-Apr-2021.)
Assertion
Ref Expression
equequ2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))

Proof of Theorem equequ2
StepHypRef Expression
1 equtrr 1995 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
2 equeuclr 1996 . 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:  ax13lem2  2332  axc15  2339  dveeq2ALT  2371  eujust  2500  eujustALT  2501  euequ1  2504  euf  2506  mo2  2507  eleq1w  2713  disjxun  4683  axrep2  4806  dtru  4887  zfpair  4934  dfid3  5054  isso2i  5096  iotaval  5900  dff13f  6553  dfwe2  7023  aceq0  8979  zfac  9320  axpowndlem4  9460  zfcndac  9479  injresinj  12629  infpn2  15664  ramub1lem2  15778  fullestrcsetc  16838  fullsetcestrc  16853  symgextf1  17887  mplcoe1  19513  evlslem2  19560  mamulid  20295  mamurid  20296  mdetdiagid  20454  dscmet  22424  lgseisenlem2  25146  dchrisumlem3  25225  frgr2wwlk1  27309  bj-ssbjust  32743  bj-ssbequ  32754  bj-ssblem1  32755  bj-ssblem2  32756  bj-ssb1a  32757  bj-ssb1  32758  bj-ssbcom3lem  32775  bj-axrep2  32914  bj-dtru  32922  bj-ax8  33012  wl-aleq  33452  wl-mo2df  33482  wl-eudf  33484  wl-euequ1f  33486  wl-mo2t  33487  dveeq2-o  34537  axc11n-16  34542  ax12eq  34545  ax12inda  34552  ax12v2-o  34553  fphpd  37697  iotavalb  38948  disjinfi  39694
  Copyright terms: Public domain W3C validator