![]() |
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 2722 reu8 2934 sbcco2 2986 snnex 4449 tfisi 4587 opeliunxp 4682 elrnmpt1 4879 rnxpid 5064 iotaval 5190 elabrex 5759 opabex3d 6122 opabex3 6123 enq0ref 7432 fproddivapf 11639 setindis 14722 bdsetindis 14724 |
Copyright terms: Public domain | W3C validator |