Theorem equcomi 1684

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 1681	. 2 |- x = x
2		ax-8 1484	. 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 105  ax-gen 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax6evr  1685  equcom  1686  equcoms  1688  ax10  1697  cbv2h  1728  cbv2w  1730  equvini  1738  equveli  1739  equsb2  1766  drex1  1778  sbcof2  1790  aev  1792  cbvexdh  1906  rext  4176  iotaval  5147  prodmodc  11479