Theorem equcomi 2016

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 2011	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2015	. 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 2007

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

This theorem is referenced by:  equcom  2017  equcoms  2019  ax13dgen2  2138  sbequ2  2249  cbv2w  2338  cbv2  2407  cbv2h  2410  axc16i  2440  equvini  2459  equsb2  2496  axsepgfromrep  5264  rext  5423  dfid2  5550  soxp  8128  xpord3inddlem  8153  axextnd  10605  prodmo  15952  mpomatmul  22384  cbvex1v  35105  finminlem  36336  bj-ssbid2ALT  36681  axc11n11  36700  axc11n11r  36701  bj-cbv2hv  36815  ax6er  36851  bj-dfid2ALT  37083  bj-imdiridlem  37203  wl-axc11rc11  37601  poimirlem25  37669  axc11nfromc11  38944  aev-o  38949  oppcendc  48993