New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 | ⊢ (x = y → φ) |
Ref | Expression |
---|---|
equcoms | ⊢ (y = x → φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcomi 1679 | . 2 ⊢ (y = x → x = y) | |
2 | equcoms.1 | . 2 ⊢ (x = y → φ) | |
3 | 1, 2 | syl 15 | 1 ⊢ (y = x → φ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: equtr 1682 equtr2 1688 ax12b 1689 ax12bOLD 1690 spfw 1691 spw 1694 cbvalw 1701 cbvalvw 1702 alcomiw 1704 elequ1 1713 elequ2 1715 stdpc7 1917 sbequ12r 1920 sbequ12a 1921 ax12olem1 1927 ax12 1935 ax10o 1952 cbval 1984 equvini 1987 sbequ 2060 sb6rf 2091 sb6a 2116 ax12from12o 2156 ax10o-o 2203 mo 2226 cleqh 2450 cbvab 2471 sbralie 2848 reu8 3032 opeliunxp 4820 addccan2nclem1 6263 |
Copyright terms: Public domain | W3C validator |