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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  equcom  2017  equcoms  2019  ax13dgen2  2138  sbequ2  2249  cbv2w  2339  cbv2  2408  cbv2h  2411  axc16i  2441  equvini  2460  equsb2  2497  axsepgfromrep  5294  rext  5453  dfid2  5580  soxp  8154  xpord3inddlem  8179  axextnd  10631  prodmo  15972  mpomatmul  22452  cbvex1v  35088  finminlem  36319  bj-ssbid2ALT  36664  axc11n11  36683  axc11n11r  36684  bj-cbv2hv  36798  ax6er  36834  bj-dfid2ALT  37066  bj-imdiridlem  37186  wl-axc11rc11  37584  poimirlem25  37652  axc11nfromc11  38927  aev-o  38932  oppcendc  48906