Theorem equcomi 1931

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 1926	. 2 ⊢ 𝑥 = 𝑥
2		ax7 1930	. 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 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  equcom  1932  equcoms  1934  ax13dgen2  2002  cbv2h  2257  axc11nOLD  2296  axc11nOLDOLD  2297  axc11nALT  2298  axc16i  2310  equsb2  2357  axsep  4708  rext  4843  iotaval  5779  soxp  7177  axextnd  9292  prodmo  14505  mpt2matmul  20071  finminlem  31482  bj-ssbid2ALT  31835  axc11n11  31859  axc11n11r  31860  bj-cbv2hv  31918  bj-axsep  31981  ax6er  32008  poimirlem25  32604  axc11nfromc11  33229  aev-o  33234