Theorem equcomi 2017

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 2012	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2016	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  equcom  2018  equcoms  2020  ax13dgen2  2139  sbequ2  2250  cbv2w  2335  cbv2  2401  cbv2h  2404  axc16i  2434  equvini  2453  equsb2  2490  axsepgfromrep  5244  rext  5403  dfid2  5528  soxp  8085  xpord3inddlem  8110  axextnd  10520  prodmo  15878  mpomatmul  22309  cbvex1v  35037  finminlem  36279  bj-ssbid2ALT  36624  axc11n11  36643  axc11n11r  36644  bj-cbv2hv  36758  ax6er  36794  bj-dfid2ALT  37026  bj-imdiridlem  37146  wl-axc11rc11  37544  poimirlem25  37612  axc11nfromc11  38892  aev-o  38897  oppcendc  48980