Theorem equcomi 2044

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 2039	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2043	. 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 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

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

This theorem is referenced by:  equcom  2045  equcoms  2047  ax13dgen2  2179  sbequ2  2291  cbv2w  2375  cbv2  2441  cbv2h  2444  axc16i  2474  equvini  2493  equsb2  2530  axsepgfromrep  5256  rext  5427  dfid2  5556  soxp  8121  xpord3inddlem  8146  axextnd  10572  prodmo  15986  mpomatmul  22568  cbvex1v  35403  finminlem  36714  bj-ssbid2ALT  37170  axc11n11  37192  axc11n11r  37193  bj-nnf-cbval  37290  bj-cbv2hv  37317  ax6er  37353  bj-dfid2ALT  37585  bj-imdiridlem  37712  wl-axc11rc11  38121  poimirlem25  38179  axc11nfromc11  39585  aev-o  39590  oppcendc  49676