Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > equcomi | Unicode 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 1681 | . 2 | |
2 | ax-8 1484 | . 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 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 |
Copyright terms: Public domain | W3C validator |