Theorem equcomi 2024

Description: Commutative law for equality. Equality is a symmetric relation. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 10-Jan-1993.) (Revised by NM, 9-Apr-2017.)

Assertion

Ref	Expression
equcomi	⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Proof of Theorem equcomi

Step	Hyp	Ref	Expression
1		equid 2019	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2023	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥))
3	1, 2	mpi 20	1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781

This theorem is referenced by:  equcom  2025  equcoms  2027  ax13dgen2  2142  sbequ2  2250  sbequ2OLD  2251  cbv2w  2357  cbv2  2423  cbv2h  2426  axc16i  2458  equvini  2477  equsb2  2531  vtoclgft  3553  axsepgfromrep  5201  rext  5341  soxp  7823  axextnd  10013  prodmo  15290  mpomatmul  21055  finminlem  33666  bj-ssbid2ALT  33996  axc11n11  34016  axc11n11r  34017  bj-cbv2hv  34119  ax6er  34156  wl-axc11rc11  34830  poimirlem25  34932  axc11nfromc11  36077  aev-o  36082