Theorem equcomi 2018

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 2013	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2017	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  equcom  2019  equcoms  2021  ax13dgen2  2143  sbequ2  2256  cbv2w  2341  cbv2  2407  cbv2h  2410  axc16i  2440  equvini  2459  equsb2  2496  axsepgfromrep  5239  rext  5396  dfid2  5521  soxp  8071  xpord3inddlem  8096  axextnd  10502  prodmo  15859  mpomatmul  22390  cbvex1v  35230  finminlem  36512  bj-ssbid2ALT  36864  axc11n11  36883  axc11n11r  36884  bj-cbv2hv  36998  ax6er  37034  bj-dfid2ALT  37266  bj-imdiridlem  37390  wl-axc11rc11  37788  poimirlem25  37846  axc11nfromc11  39186  aev-o  39191  oppcendc  49263