Theorem equcomi 2013

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 2008	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2012	. 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 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775

This theorem is referenced by:  equcom  2014  equcoms  2016  ax13dgen2  2130  sbequ2  2240  cbv2w  2331  cbv2  2400  cbv2h  2403  axc16i  2433  equvini  2452  equsb2  2489  axsepgfromrep  5303  rext  5456  dfid2  5584  soxp  8148  xpord3inddlem  8173  axextnd  10635  prodmo  15951  mpomatmul  22439  cbvex1v  34950  finminlem  36071  bj-ssbid2ALT  36409  axc11n11  36428  axc11n11r  36429  bj-cbv2hv  36543  ax6er  36579  bj-dfid2ALT  36812  bj-imdiridlem  36932  wl-axc11rc11  37318  poimirlem25  37386  axc11nfromc11  38664  aev-o  38669