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  2401  cbv2h  2404  axc16i  2434  equvini  2453  equsb2  2490  axsepgfromrep  5249  rext  5408  dfid2  5535  soxp  8108  xpord3inddlem  8133  axextnd  10544  prodmo  15902  mpomatmul  22333  cbvex1v  35064  finminlem  36306  bj-ssbid2ALT  36651  axc11n11  36670  axc11n11r  36671  bj-cbv2hv  36785  ax6er  36821  bj-dfid2ALT  37053  bj-imdiridlem  37173  wl-axc11rc11  37571  poimirlem25  37639  axc11nfromc11  38919  aev-o  38924  oppcendc  49007