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 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  equcom  2025  equcoms  2027  ax13dgen2  2139  sbequ2  2247  sbequ2OLD  2248  cbv2w  2346  cbv2  2412  cbv2h  2415  axc16i  2447  equvini  2466  equsb2  2510  vtoclgft  3501  axsepgfromrep  5165  rext  5306  soxp  7806  axextnd  10002  prodmo  15282  mpomatmul  21051  finminlem  33779  bj-ssbid2ALT  34109  axc11n11  34129  axc11n11r  34130  bj-cbv2hv  34234  ax6er  34271  bj-imdiridlem  34600  wl-axc11rc11  34980  poimirlem25  35082  axc11nfromc11  36222  aev-o  36227