Theorem equcomi 2036

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 2031	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2035	. 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 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  equcom  2037  equcoms  2039  ax13dgen2  2171  sbequ2  2283  cbv2w  2367  cbv2  2433  cbv2h  2436  axc16i  2466  equvini  2485  equsb2  2522  axsepgfromrep  5241  rext  5412  dfid2  5540  soxp  8103  xpord3inddlem  8128  axextnd  10543  prodmo  15957  mpomatmul  22494  cbvex1v  35330  finminlem  36639  bj-ssbid2ALT  37096  axc11n11  37118  axc11n11r  37119  bj-nnf-cbval  37216  bj-cbv2hv  37243  ax6er  37279  bj-dfid2ALT  37511  bj-imdiridlem  37638  wl-axc11rc11  38047  poimirlem25  38105  axc11nfromc11  39511  aev-o  39516  oppcendc  49600