Theorem equcomi 1124

Description: Commutative law for equality. Lemma 7 of [Tarski] p. 69.

Assertion

Ref	Expression
equcomi	|- (x = y -> y = x)

Proof of Theorem equcomi

Step	Hyp	Ref	Expression
1		equid 1122	. 2 |- x = x
2		ax-8 961	. 2 |- (x = y -> (x = x -> y = x))
3	1, 2	mpi 44	1 |- (x = y -> y = x)

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  equcom 1125  equcoms 1126  equtr2 1129  ax10 1137  cbv2 1159  equvini 1164  equsb2 1190  aev 1204  a16g 1271  axsep 2692  rext 2744  ider 4253  unxpdomlem 4815  axextnd 4915

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-8 961  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

Copyright terms: Public domain