![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > equcoms | Unicode version |
Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
equcoms.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
equcoms |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcomi 1715 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equcoms.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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-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: equtr 1720 equtr2 1722 equequ2 1724 ax10o 1726 cbvalv1 1762 cbvexv1 1763 cbvalh 1764 cbvexh 1766 equvini 1769 stdpc7 1781 sbequ12r 1783 sbequ12a 1784 sbequ 1851 sb6rf 1864 cbvalvw 1931 cbvexvw 1932 sb9v 1990 sb6a 2000 mo2n 2066 elequ1 2164 elequ2 2165 cleqh 2289 cbvab 2313 sbralie 2736 reu8 2948 sbcco2 3000 snnex 4466 tfisi 4604 opeliunxp 4699 elrnmpt1 4896 rnxpid 5081 iotaval 5207 elabrex 5778 elabrexg 5779 opabex3d 6145 opabex3 6146 enq0ref 7461 fproddivapf 11670 setindis 15172 bdsetindis 15174 |
Copyright terms: Public domain | W3C validator |