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

Theorem equequ2 2024
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 2020 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
2 equeuclr 2021 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑦𝑧 = 𝑥))
31, 2impbid 213 1 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772
This theorem is referenced by:  sbjust  2059  sbequ  2081  sb6  2084  equsb3r  2101  ax13lem2  2387  axc15OLD  2439  dveeq2ALT  2471  sb4b  2495  sb4bOLD  2496  mojust  2617  mof  2643  eujust  2652  eujustALT  2653  eu6lem  2654  euf  2657  eleq1w  2895  disjxun  5056  axrep2  5185  dtru  5263  zfpair  5313  dfid3  5456  isso2i  5502  iotaval  6323  dff13f  7005  dfwe2  7484  aceq0  9533  zfac  9871  axpowndlem4  10011  zfcndac  10030  injresinj  13148  infpn2  16239  ramub1lem2  16353  fullestrcsetc  17391  fullsetcestrc  17406  symgextf1  18480  mplcoe1  20176  evlslem2  20222  mamulid  20980  mamurid  20981  mdetdiagid  21139  dscmet  23111  lgseisenlem2  25880  dchrisumlem3  25995  frgr2wwlk1  28036  bj-ssblem1  33885  bj-ssblem2  33886  bj-ax12  33888  bj-dtru  34037  wl-aleq  34657  wl-mo2df  34688  wl-eudf  34690  wl-euequf  34692  wl-mo2t  34693  dveeq2-o  35951  axc11n-16  35956  ax12eq  35959  ax12inda  35966  ax12v2-o  35967  fphpd  39293  iotavalb  40642  disjinfi  41334  eusnsn  43142  2reu8i  43193  2reuimp0  43194  ichexmpl1  43478
  Copyright terms: Public domain W3C validator