Theorem equcomi 2047

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 2042	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2046	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥))
3	1, 2	mpi 21	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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  equcom  2048  equcoms  2050  ax13dgen2  2173  sbequ2  2285  cbv2w  2369  cbv2  2435  cbv2h  2438  axc16i  2468  equvini  2487  equsb2  2524  axsepgfromrep  5255  rext  5429  dfid2  5558  soxp  8121  xpord3inddlem  8146  axextnd  10571  prodmo  15986  mpomatmul  22603  cbvex1v  35462  finminlem  36829  bj-ssbid2ALT  37285  axc11n11  37307  axc11n11r  37308  bj-nnf-cbval  37405  bj-cbv2hv  37432  ax6er  37468  bj-dfid2ALT  37701  bj-imdiridlem  37829  wl-axc11rc11  38238  poimirlem25  38296  axc11nfromc11  39700  aev-o  39705  oppcendc  49796