Theorem equequ2 1984

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

Step	Hyp	Ref	Expression
1		equtrr 1980	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 1981	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	1, 2	impbid 204	1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744

This theorem is referenced by:  sbjust  2015  sbequ  2036  sb6  2038  equsb3r  2047  ax13lem2  2306  axc15OLD  2359  dveeq2ALT  2391  sb4b  2425  mojust  2550  mof  2580  mofOLD  2581  eujust  2591  eujustALT  2592  eu6lem  2593  eu6OLDOLD  2597  euf  2598  eufOLD  2599  euequOLD  2621  eleq1w  2850  disjxun  4932  axrep2  5056  dtru  5128  zfpair  5182  dfid3  5317  isso2i  5364  iotaval  6168  dff13f  6845  dfwe2  7318  aceq0  9344  zfac  9686  axpowndlem4  9826  zfcndac  9845  injresinj  12979  infpn2  16111  ramub1lem2  16225  fullestrcsetc  17271  fullsetcestrc  17286  symgextf1  18322  mplcoe1  19971  evlslem2  20017  mamulid  20769  mamurid  20770  mdetdiagid  20928  dscmet  22900  lgseisenlem2  25669  dchrisumlem3  25784  frgr2wwlk1  27878  bj-ssblem1  33535  bj-ssblem2  33536  bj-ax12  33538  bj-axrep2  33659  bj-dtru  33665  wl-aleq  34257  wl-mo2df  34287  wl-eudf  34289  wl-euequf  34291  wl-mo2t  34292  dveeq2-o  35554  axc11n-16  35559  ax12eq  35562  ax12inda  35569  ax12v2-o  35570  fphpd  38850  iotavalb  40220  disjinfi  40915  eusnsn  42701  2reu8i  42753  2reuimp0  42754  ichexmpl1  43034