Theorem equequ2 1940

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

Syntax hints:   → wi 4   ↔ wb 195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  axc11nlemOLD2  1975  ax12vOLDOLD  2038  axc11nlemOLD  2146  ax13lem2  2284  axc15  2291  axc11nlemALT  2294  dveeq2ALT  2328  ax12v2OLD  2330  eujust  2460  eujustALT  2461  euequ1  2464  euf  2466  mo2  2467  disjxun  4581  axrep2  4701  dtru  4783  zfpair  4831  dfid3  4954  isso2i  4991  iotaval  5779  dff13f  6417  dfwe2  6873  aceq0  8824  zfac  9165  axpowndlem4  9301  zfcndac  9320  injresinj  12451  infpn2  15455  ramub1lem2  15569  fullestrcsetc  16614  fullsetcestrc  16629  symgextf1  17664  mplcoe1  19286  evlslem2  19333  mamulid  20066  mamurid  20067  mdetdiagid  20225  dscmet  22187  lgseisenlem2  24901  dchrisumlem3  24980  usgrasscusgra  26011  bj-ssbequ  31818  bj-ssblem1  31819  bj-ssblem2  31820  bj-ssb1a  31821  bj-ssb1  31822  bj-ssbcom3lem  31839  bj-axrep2  31977  bj-dtru  31985  bj-eleq1w  32040  bj-ax8  32080  wl-aleq  32501  wl-mo2df  32531  wl-eudf  32533  wl-euequ1f  32535  wl-mo2t  32536  dveeq2-o  33236  axc11n-16  33241  ax12eq  33244  ax12inda  33251  ax12v2-o  33252  fphpd  36398  iotavalb  37653  disjinfi  38375