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  2402  cbv2h  2405  axc16i  2435  equvini  2454  equsb2  2491  axsepgfromrep  5252  rext  5411  dfid2  5538  soxp  8111  xpord3inddlem  8136  axextnd  10551  prodmo  15909  mpomatmul  22340  cbvex1v  35071  finminlem  36313  bj-ssbid2ALT  36658  axc11n11  36677  axc11n11r  36678  bj-cbv2hv  36792  ax6er  36828  bj-dfid2ALT  37060  bj-imdiridlem  37180  wl-axc11rc11  37578  poimirlem25  37646  axc11nfromc11  38926  aev-o  38931  oppcendc  49011