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  2143  sbequ2  2254  cbv2w  2339  cbv2  2405  cbv2h  2408  axc16i  2438  equvini  2457  equsb2  2494  axsepgfromrep  5236  rext  5393  dfid2  5518  soxp  8068  xpord3inddlem  8093  axextnd  10493  prodmo  15850  mpomatmul  22381  cbvex1v  35158  finminlem  36434  bj-ssbid2ALT  36780  axc11n11  36799  axc11n11r  36800  bj-cbv2hv  36914  ax6er  36950  bj-dfid2ALT  37182  bj-imdiridlem  37302  wl-axc11rc11  37700  poimirlem25  37758  axc11nfromc11  39098  aev-o  39103  oppcendc  49179