Theorem equcomi 2021

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 2016	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2020	. 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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  equcom  2022  equcoms  2024  ax13dgen2  2136  sbequ2  2244  sbequ2OLD  2245  cbv2w  2336  cbv2  2403  cbv2h  2406  axc16i  2436  equvini  2455  equsb2  2496  vtoclgft  3482  axsepgfromrep  5216  rext  5358  dfid2  5482  soxp  7941  axextnd  10278  prodmo  15574  mpomatmul  21503  finminlem  34434  bj-ssbid2ALT  34771  axc11n11  34791  axc11n11r  34792  bj-cbv2hv  34906  ax6er  34943  bj-dfid2ALT  35163  bj-imdiridlem  35283  wl-axc11rc11  35661  poimirlem25  35729  axc11nfromc11  36867  aev-o  36872