![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > equcom | Unicode version |
Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.) |
Ref | Expression |
---|---|
equcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcomi 1648 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equcomi 1648 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 125 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1393 ax-ie2 1438 ax-8 1450 ax-17 1474 ax-i9 1478 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: equcomd 1651 sbal1yz 1937 dveeq1 1955 eu1 1985 reu7 2832 reu8 2833 dfdif3 3133 iunid 3815 copsexg 4104 opelopabsbALT 4119 dtruex 4412 opeliunxp 4532 relop 4627 dmi 4692 opabresid 4808 intirr 4861 cnvi 4879 coi1 4990 brprcneu 5346 f1oiso 5659 qsid 6424 mapsnen 6635 summodc 10991 bezoutlemle 11489 cnmptid 12231 |
Copyright terms: Public domain | W3C validator |