Theorem equcomi 1115

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 1113	. 2 |- x = x
2		ax-8 1101	. 2 |- (x = y -> (x = x -> y = x))
3	1, 2	mpi 44	1 |- (x = y -> y = x)

Syntax hints:   -> wi 3   = wceq 1099

This theorem is referenced by:  equcom 1116  equcoms 1117  equtr2 1120  alequcom 1125  cbv2 1146  equvini 1151  equsb2 1177  aev 1192  a16g 1258  axsep 2670  rext 2722  ider 4207  unxpdomlem 4766  axextnd 4866

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-8 1101  ax-9 1102  ax-12 1104

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957

Copyright terms: Public domain