Theorem equcomi 1727

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 1724	. 2 |- x = x
2		ax-8 1527	. 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 1472  ax-ie2 1517  ax-8 1527  ax-17 1549  ax-i9 1553

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1728  equcom  1729  equcoms  1731  ax10  1740  cbv2h  1771  cbv2w  1773  equvini  1781  equveli  1782  equsb2  1809  drex1  1821  sbcof2  1833  aev  1835  cbvexdh  1950  rext  4259  iotaval  5243  prodmodc  11889