Theorem equcomi 1165

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

Syntax hints:   -> wi 3   = wceq 992

This theorem is referenced by:  equcom 1166  equcoms 1167  equtr2 1170  ax10 1178  cbv2 1200  equvini 1205  equsb2 1231  aev 1245  a16g 1314  axsep 2776  rext 2834  ider 4409  unxpdomlem 4993  axextnd 5097  inpc 10867

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-8 1000  ax-12 1004  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159

Copyright terms: Public domain