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  2385  axc15OLD  2436  dveeq2ALT  2468  sb4b  2492  sb4bOLD  2493  mojust  2614  mof  2640  eujust  2649  eujustALT  2650  eu6lem  2651  euf  2654  eleq1w  2892  disjxun  5055  axrep2  5184  dtru  5262  zfpair  5312  dfid3  5455  isso2i  5501  iotaval  6322  dff13f  7005  dfwe2  7485  aceq0  9532  zfac  9870  axpowndlem4  10010  zfcndac  10029  injresinj  13146  infpn2  16237  ramub1lem2  16351  fullestrcsetc  17389  fullsetcestrc  17404  symgextf1  18478  mplcoe1  20174  evlslem2  20220  mamulid  20978  mamurid  20979  mdetdiagid  21137  dscmet  23109  lgseisenlem2  25879  dchrisumlem3  25994  frgr2wwlk1  28035  bj-ssblem1  33884  bj-ssblem2  33885  bj-ax12  33887  bj-dtru  34036  wl-aleq  34656  wl-mo2df  34687  wl-eudf  34689  wl-euequf  34691  wl-mo2t  34692  dveeq2-o  35949  axc11n-16  35954  ax12eq  35957  ax12inda  35964  ax12v2-o  35965  fphpd  39291  iotavalb  40639  disjinfi  41330  eusnsn  43138  2reu8i  43189  2reuimp0  43190  ichexmpl1  43508
  Copyright terms: Public domain W3C validator