![]() |
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 1715 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equcomi 1715 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 126 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1460 ax-ie2 1505 ax-8 1515 ax-17 1537 ax-i9 1541 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: equcomd 1718 sbal1yz 2013 dveeq1 2031 eu1 2063 reu7 2947 reu8 2948 dfdif3 3260 iunid 3957 copsexg 4262 opelopabsbALT 4277 dtruex 4576 opeliunxp 4699 relop 4795 dmi 4860 opabresid 4978 intirr 5033 cnvi 5051 coi1 5162 brprcneu 5527 f1oiso 5848 qsid 6626 mapsnen 6837 suplocsrlem 7837 summodc 11423 bezoutlemle 12041 cnmptid 14238 |
Copyright terms: Public domain | W3C validator |