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

Theorem equequ2 1939
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 1935 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
2 equeuclr 1936 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑦𝑧 = 𝑥))
31, 2impbid 200 1 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  axc11nlemOLD2  1974  ax12vOLDOLD  2036  axc11nlemOLD  2142  ax13lem2  2279  axc9lem2OLD  2280  axc15  2287  axc11nlemALT  2290  dveeq2ALT  2324  ax12v2OLD  2326  eujust  2456  eujustALT  2457  euequ1  2460  euf  2462  mo2  2463  disjxun  4572  axrep2  4692  dtru  4775  zfpair  4823  dfid3  4941  isso2i  4978  iotaval  5762  dff13f  6392  dfwe2  6847  aceq0  8798  zfac  9139  axpowndlem4  9275  zfcndac  9294  injresinj  12403  infpn2  15398  ramub1lem2  15512  fullestrcsetc  16557  fullsetcestrc  16572  symgextf1  17607  mplcoe1  19229  evlslem2  19276  mamulid  20005  mamurid  20006  mdetdiagid  20164  dscmet  22125  lgseisenlem2  24815  dchrisumlem3  24894  usgrasscusgra  25774  bj-ssbequ  31621  bj-ssblem1  31622  bj-ssblem2  31623  bj-ssb1a  31624  bj-ssb1  31625  bj-ssbcom3lem  31642  bj-axc15v  31744  bj-axrep2  31787  bj-dtru  31795  bj-eleq1w  31840  bj-ax8  31880  wl-aleq  32301  wl-mo2df  32331  wl-eudf  32333  wl-euequ1f  32335  wl-mo2t  32336  dveeq2-o  33036  axc11n-16  33041  ax12eq  33044  ax12inda  33051  ax12v2-o  33052  fphpd  36198  iotavalb  37453  disjinfi  38175
  Copyright terms: Public domain W3C validator