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  2341  cbv2  2407  cbv2h  2410  axc16i  2440  equvini  2459  equsb2  2496  axsepgfromrep  5229  rext  5400  dfid2  5528  soxp  8079  xpord3inddlem  8104  axextnd  10514  prodmo  15901  mpomatmul  22411  cbvex1v  35216  finminlem  36500  bj-ssbid2ALT  36957  axc11n11  36979  axc11n11r  36980  bj-nnf-cbval  37077  bj-cbv2hv  37104  ax6er  37140  bj-dfid2ALT  37372  bj-imdiridlem  37499  wl-axc11rc11  37908  poimirlem25  37966  axc11nfromc11  39372  aev-o  39377  oppcendc  49493