Theorem equcomi 1944

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 1939	. 2 ⊢ 𝑥 = 𝑥
2		ax7 1943	. 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 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  equcom  1945  equcoms  1947  ax13dgen2  2015  cbv2h  2269  axc11nOLD  2308  axc11nOLDOLD  2309  axc11nALT  2310  axc16i  2322  equsb2  2369  axsep  4780  rext  4916  soxp  7290  axextnd  9413  prodmo  14666  mpt2matmul  20252  finminlem  32312  bj-ssbid2ALT  32646  axc11n11  32672  axc11n11r  32673  bj-cbv2hv  32731  bj-axsep  32793  ax6er  32820  poimirlem25  33434  axc11nfromc11  34211  aev-o  34216