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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  equcom  2025  equcoms  2027  ax13dgen2  2149  sbequ2  2261  cbv2w  2345  cbv2  2411  cbv2h  2414  axc16i  2444  equvini  2463  equsb2  2500  axsepgfromrep  5216  rext  5387  dfid2  5515  soxp  8069  xpord3inddlem  8094  axextnd  10505  prodmo  15892  mpomatmul  22429  cbvex1v  35256  finminlem  36546  bj-ssbid2ALT  37003  axc11n11  37025  axc11n11r  37026  bj-nnf-cbval  37123  bj-cbv2hv  37150  ax6er  37186  bj-dfid2ALT  37418  bj-imdiridlem  37545  wl-axc11rc11  37954  poimirlem25  38012  axc11nfromc11  39418  aev-o  39423  oppcendc  49508