![]() |
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 4447 tfisi 4585 opeliunxp 4680 elrnmpt1 4877 rnxpid 5062 iotaval 5188 elabrex 5756 opabex3d 6119 opabex3 6120 enq0ref 7429 fproddivapf 11632 setindis 14579 bdsetindis 14581 |
Copyright terms: Public domain | W3C validator |