Theorem equequ2 2121

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 2117	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2118	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	1, 2	impbid 203	1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860

This theorem is referenced by:  ax13lem2  2462  axc15  2470  dveeq2ALT  2501  eujust  2631  eujustALT  2632  euequ1  2635  euf  2637  mo2  2638  eleq1w  2864  disjxun  4835  axrep2  4960  dtru  5034  zfpair  5088  dfid3  5214  isso2i  5258  iotaval  6069  dff13f  6731  dfwe2  7205  aceq0  9218  zfac  9561  axpowndlem4  9701  zfcndac  9720  injresinj  12807  infpn2  15828  ramub1lem2  15942  fullestrcsetc  16990  fullsetcestrc  17005  symgextf1  18036  mplcoe1  19668  evlslem2  19714  mamulid  20451  mamurid  20452  mdetdiagid  20611  dscmet  22584  lgseisenlem2  25309  dchrisumlem3  25388  frgr2wwlk1  27498  bj-ssbjust  32928  bj-ssbequ  32939  bj-ssblem1  32940  bj-ssblem2  32941  bj-ssb1a  32942  bj-ssb1  32943  bj-ssbcom3lem  32959  bj-axrep2  33097  bj-dtru  33105  bj-ax8  33189  wl-aleq  33630  wl-mo2df  33660  wl-eudf  33662  wl-euequ1f  33664  wl-mo2t  33665  dveeq2-o  34706  axc11n-16  34711  ax12eq  34714  ax12inda  34721  ax12v2-o  34722  fphpd  37876  iotavalb  39124  disjinfi  39863  eusnsn  41644