Theorem equcomi 1704

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 1701	. 2 |- x = x
2		ax-8 1504	. 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 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1705  equcom  1706  equcoms  1708  ax10  1717  cbv2h  1748  cbv2w  1750  equvini  1758  equveli  1759  equsb2  1786  drex1  1798  sbcof2  1810  aev  1812  cbvexdh  1926  rext  4213  iotaval  5186  prodmodc  11577