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  5236  rext  5395  dfid2  5520  soxp  8069  xpord3inddlem  8094  axextnd  10504  prodmo  15862  mpomatmul  22350  cbvex1v  35060  finminlem  36311  bj-ssbid2ALT  36656  axc11n11  36675  axc11n11r  36676  bj-cbv2hv  36790  ax6er  36826  bj-dfid2ALT  37058  bj-imdiridlem  37178  wl-axc11rc11  37576  poimirlem25  37644  axc11nfromc11  38924  aev-o  38929  oppcendc  49023