Theorem equcomi 2019

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 2014	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2018	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  equcom  2020  equcoms  2022  ax13dgen2  2144  sbequ2  2257  cbv2w  2342  cbv2  2408  cbv2h  2411  axc16i  2441  equvini  2460  equsb2  2497  axsepgfromrep  5241  rext  5403  dfid2  5529  soxp  8081  xpord3inddlem  8106  axextnd  10514  prodmo  15871  mpomatmul  22402  cbvex1v  35250  finminlem  36534  bj-ssbid2ALT  36908  axc11n11  36927  axc11n11r  36928  bj-cbv2hv  37045  ax6er  37081  bj-dfid2ALT  37313  bj-imdiridlem  37440  wl-axc11rc11  37838  poimirlem25  37896  axc11nfromc11  39302  aev-o  39307  oppcendc  49377