![]() |
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 | ⊢ (x = y → φ) |
Ref | Expression |
---|---|
equcoms | ⊢ (y = x → φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcomi 1589 | . 2 ⊢ (y = x → x = y) | |
2 | equcoms.1 | . 2 ⊢ (x = y → φ) | |
3 | 1, 2 | syl 14 | 1 ⊢ (y = x → φ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-gen 1335 ax-ie2 1380 ax-8 1392 ax-17 1416 ax-i9 1420 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: equtr 1592 equtr2 1594 equequ2 1596 elequ1 1597 elequ2 1598 ax10o 1600 cbvalh 1633 cbvexh 1635 equvini 1638 stdpc7 1650 sbequ12r 1652 sbequ12a 1653 sbequ 1718 sb6rf 1730 sb9v 1851 sb6a 1861 mo2n 1925 cleqh 2134 cbvab 2157 reu8 2731 sbcco2 2780 snnex 4147 tfisi 4253 opeliunxp 4338 elrnmpt1 4528 rnxpid 4698 iotaval 4821 elabrex 5340 opabex3d 5690 opabex3 5691 enq0ref 6416 setindis 9427 bdsetindis 9429 |
Copyright terms: Public domain | W3C validator |