Theorem equequ2 2053

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807

This theorem is referenced by:  rename-sb  2096  sbequ  2123  sb6  2125  equsb3r  2145  ax13lem2  2414  dveeq2ALT  2492  sb4b  2513  mojust  2572  mof  2597  eujust  2605  eujustALT  2606  eu6lem  2607  euf  2610  eleq1w  2852  mo2icl  3686  disjxun  5108  axrep2  5242  dtruALT2  5339  zfpair  5390  dfid3  5557  solin  5594  isso2i  5604  dff13f  7251  dfwe2  7769  poxp2  8135  poxp3  8142  aceq0  10098  zfac  10440  axpowndlem4  10581  zfcndac  10600  injresinj  13816  infpn2  16969  ramub1lem2  17083  fullestrcsetc  18203  fullsetcestrc  18218  symgextf1  19487  mplcoe1  22153  evlslem2  22195  mamulid  22563  mamurid  22564  mdetdiagid  22722  dscmet  24694  lgseisenlem2  27502  dchrisumlem3  27617  frgr2wwlk1  30617  sbequbidv  36611  cbvsbdavw2  36652  axtcond  36874  dfttc4  36926  mh-setindnd  36933  bj-ssblem1  37161  bj-ssblem2  37162  bj-ax12  37164  wl-aleq  38073  wl-mo2df  38108  wl-eudf  38110  wl-euequf  38112  wl-mo2t  38113  dveeq2-o  39592  axc11n-16  39597  ax12eq  39600  ax12inda  39607  ax12v2-o  39608  aks6d1c6lem3  42824  fsuppind  43209  eu6w  43295  fphpd  43430  iotavalb  45027  disjinfi  45797  eusnsn  47647  fcoresf1  47690  2reu8i  47734  2reuimp0  47735  ichexmpl1  48102  nprmmul3  48162