Theorem equcomi 2016

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 2011	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2015	. 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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  equcom  2017  equcoms  2019  ax13dgen2  2138  sbequ2  2250  cbv2w  2343  cbv2  2411  cbv2h  2414  axc16i  2444  equvini  2463  equsb2  2500  axsepgfromrep  5315  rext  5468  dfid2  5595  soxp  8170  xpord3inddlem  8195  axextnd  10660  prodmo  15984  mpomatmul  22473  cbvex1v  35050  finminlem  36284  bj-ssbid2ALT  36629  axc11n11  36648  axc11n11r  36649  bj-cbv2hv  36763  ax6er  36799  bj-dfid2ALT  37031  bj-imdiridlem  37151  wl-axc11rc11  37537  poimirlem25  37605  axc11nfromc11  38882  aev-o  38887