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 1665 | . 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 105 ax-gen 1410 ax-ie2 1455 ax-8 1467 ax-17 1491 ax-i9 1495 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: equtr 1670 equtr2 1672 equequ2 1674 elequ1 1675 elequ2 1676 ax10o 1678 cbvalh 1711 cbvexh 1713 equvini 1716 stdpc7 1728 sbequ12r 1730 sbequ12a 1731 sbequ 1796 sb6rf 1809 sb9v 1931 sb6a 1941 mo2n 2005 cleqh 2217 cbvab 2240 sbralie 2644 reu8 2853 sbcco2 2904 snnex 4339 tfisi 4471 opeliunxp 4564 elrnmpt1 4760 rnxpid 4943 iotaval 5069 elabrex 5627 opabex3d 5987 opabex3 5988 enq0ref 7209 setindis 13061 bdsetindis 13063 |
Copyright terms: Public domain | W3C validator |