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 1691 | . 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 1436 ax-ie2 1481 ax-8 1491 ax-17 1513 ax-i9 1517 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: equtr 1696 equtr2 1698 equequ2 1700 ax10o 1702 cbvalv1 1738 cbvexv1 1739 cbvalh 1740 cbvexh 1742 equvini 1745 stdpc7 1757 sbequ12r 1759 sbequ12a 1760 sbequ 1827 sb6rf 1840 cbvalvw 1906 cbvexvw 1907 sb9v 1965 sb6a 1975 mo2n 2041 elequ1 2139 elequ2 2140 cleqh 2264 cbvab 2288 sbralie 2705 reu8 2917 sbcco2 2968 snnex 4420 tfisi 4558 opeliunxp 4653 elrnmpt1 4849 rnxpid 5032 iotaval 5158 elabrex 5720 opabex3d 6081 opabex3 6082 enq0ref 7365 fproddivapf 11558 setindis 13690 bdsetindis 13692 |
Copyright terms: Public domain | W3C validator |