![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > equcoms | GIF 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 1704 | . 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦) | |
2 | equcoms.1 | . 2 ⊢ (𝑥 = 𝑦 → 𝜑) | |
3 | 1, 2 | syl 14 | 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 106 ax-gen 1449 ax-ie2 1494 ax-8 1504 ax-17 1526 ax-i9 1530 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: equtr 1709 equtr2 1711 equequ2 1713 ax10o 1715 cbvalv1 1751 cbvexv1 1752 cbvalh 1753 cbvexh 1755 equvini 1758 stdpc7 1770 sbequ12r 1772 sbequ12a 1773 sbequ 1840 sb6rf 1853 cbvalvw 1919 cbvexvw 1920 sb9v 1978 sb6a 1988 mo2n 2054 elequ1 2152 elequ2 2153 cleqh 2277 cbvab 2301 sbralie 2721 reu8 2933 sbcco2 2985 snnex 4448 tfisi 4586 opeliunxp 4681 elrnmpt1 4878 rnxpid 5063 iotaval 5189 elabrex 5758 opabex3d 6121 opabex3 6122 enq0ref 7431 fproddivapf 11638 setindis 14689 bdsetindis 14691 |
Copyright terms: Public domain | W3C validator |