Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > equcomi | GIF version |
Description: Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
equcomi | ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equid 1694 | . 2 ⊢ 𝑥 = 𝑥 | |
2 | ax-8 1497 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥)) | |
3 | 1, 2 | mpi 15 | 1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-gen 1442 ax-ie2 1487 ax-8 1497 ax-17 1519 ax-i9 1523 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax6evr 1698 equcom 1699 equcoms 1701 ax10 1710 cbv2h 1741 cbv2w 1743 equvini 1751 equveli 1752 equsb2 1779 drex1 1791 sbcof2 1803 aev 1805 cbvexdh 1919 rext 4198 iotaval 5169 prodmodc 11528 |
Copyright terms: Public domain | W3C validator |