Theorem equcomi 1679

Description: Commutative law for equality. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 9-Apr-2017.)

Assertion

Ref	Expression
equcomi	⊢ (x = y → y = x)

Proof of Theorem equcomi

Step	Hyp	Ref	Expression
1		equid 1676	. 2 ⊢ x = x
2		ax-8 1675	. 2 ⊢ (x = y → (x = x → y = x))
3	1, 2	mpi 16	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-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  equcom  1680  equcoms  1681  equequ1OLD  1685  ax12dgen2  1726  sp  1747  spOLD  1748  dvelimhw  1849  ax12olem1  1927  ax10  1944  a16g  1945  cbv2h  1980  equvini  1987  equveli  1988  equsb2  2035  ax16i  2046  aecom-o  2151  ax10from10o  2177  aev-o  2182  iotaval  4351  ider  5944