Theorem equcomi 2019

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 2014	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2018	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  equcom  2020  equcoms  2022  ax13dgen2  2144  sbequ2  2257  cbv2w  2342  cbv2  2408  cbv2h  2411  axc16i  2441  equvini  2460  equsb2  2497  axsepgfromrep  5229  rext  5395  dfid2  5521  soxp  8072  xpord3inddlem  8097  axextnd  10505  prodmo  15892  mpomatmul  22421  cbvex1v  35232  finminlem  36516  bj-ssbid2ALT  36973  axc11n11  36995  axc11n11r  36996  bj-nnf-cbval  37093  bj-cbv2hv  37120  ax6er  37156  bj-dfid2ALT  37388  bj-imdiridlem  37515  wl-axc11rc11  37922  poimirlem25  37980  axc11nfromc11  39386  aev-o  39391  oppcendc  49505