Theorem equcomi 2018

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 2013	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2017	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  equcom  2019  equcoms  2021  ax13dgen2  2141  sbequ2  2252  cbv2w  2337  cbv2  2403  cbv2h  2406  axc16i  2436  equvini  2455  equsb2  2492  axsepgfromrep  5227  rext  5384  dfid2  5508  soxp  8054  xpord3inddlem  8079  axextnd  10477  prodmo  15838  mpomatmul  22356  cbvex1v  35078  finminlem  36352  bj-ssbid2ALT  36697  axc11n11  36716  axc11n11r  36717  bj-cbv2hv  36831  ax6er  36867  bj-dfid2ALT  37099  bj-imdiridlem  37219  wl-axc11rc11  37617  poimirlem25  37685  axc11nfromc11  38965  aev-o  38970  oppcendc  49050