Theorem equcomi 2020

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 2015	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2019	. 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 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  equcom  2021  equcoms  2023  ax13dgen2  2134  sbequ2  2241  sbequ2OLD  2242  cbv2w  2334  cbv2  2403  cbv2h  2406  axc16i  2436  equvini  2455  equsb2  2496  vtoclgft  3492  axsepgfromrep  5221  rext  5364  dfid2  5491  soxp  7970  axextnd  10347  prodmo  15646  mpomatmul  21595  finminlem  34507  bj-ssbid2ALT  34844  axc11n11  34864  axc11n11r  34865  bj-cbv2hv  34979  ax6er  35016  bj-dfid2ALT  35236  bj-imdiridlem  35356  wl-axc11rc11  35734  poimirlem25  35802  axc11nfromc11  36940  aev-o  36945