Theorem equcomi 1752

Description: Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem equcomi

Step	Hyp	Ref	Expression
1		equid 1749	. 2 |- x = x
2		ax-8 1553	. 2 |- ( x = y -> ( x = x -> y = x ) )
3	1, 2	mpi 15	1 |- ( x = y -> y = x )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1753  equcom  1754  equcoms  1756  ax10  1765  cbv2h  1797  cbv2w  1799  equvini  1807  equveli  1808  equsb2  1835  drex1  1847  sbcof2  1859  aev  1861  cbvexdh  1976  rext  4331  iotaval  5324  prodmodc  12264