Theorem equcomi 2023

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 2018	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2022	. 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 1969  ax-7 2014

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780

This theorem is referenced by:  equcom  2024  equcoms  2026  ax13dgen2  2141  sbequ2  2249  sbequ2OLD  2250  cbv2w  2356  cbv2  2422  cbv2h  2425  axc16i  2457  equvini  2476  equsb2  2530  vtoclgft  3556  axsepgfromrep  5204  rext  5344  soxp  7826  axextnd  10016  prodmo  15293  mpomatmul  21058  finminlem  33670  bj-ssbid2ALT  34000  axc11n11  34020  axc11n11r  34021  bj-cbv2hv  34123  ax6er  34160  wl-axc11rc11  34819  poimirlem25  34921  axc11nfromc11  36066  aev-o  36071