Theorem equcomi 2020

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 2015	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2019	. 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 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782

This theorem is referenced by:  equcom  2021  equcoms  2023  ax13dgen2  2134  sbequ2  2241  sbequ2OLD  2242  cbv2w  2334  cbv2  2402  cbv2h  2405  axc16i  2435  equvini  2454  equsb2  2495  vtoclgft  3505  axsepgfromrep  5246  rext  5398  dfid2  5525  soxp  8042  axextnd  10453  prodmo  15746  mpomatmul  21701  finminlem  34644  bj-ssbid2ALT  34981  axc11n11  35001  axc11n11r  35002  bj-cbv2hv  35116  ax6er  35152  bj-dfid2ALT  35390  bj-imdiridlem  35510  wl-axc11rc11  35888  poimirlem25  35956  axc11nfromc11  37242  aev-o  37247