![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > equcoms | Unicode 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 1637 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equcoms.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-gen 1383 ax-ie2 1428 ax-8 1440 ax-17 1464 ax-i9 1468 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: equtr 1642 equtr2 1644 equequ2 1646 elequ1 1647 elequ2 1648 ax10o 1650 cbvalh 1683 cbvexh 1685 equvini 1688 stdpc7 1700 sbequ12r 1702 sbequ12a 1703 sbequ 1768 sb6rf 1781 sb9v 1902 sb6a 1912 mo2n 1976 cleqh 2187 cbvab 2210 reu8 2811 sbcco2 2862 snnex 4271 tfisi 4402 opeliunxp 4493 elrnmpt1 4686 rnxpid 4865 iotaval 4991 elabrex 5537 opabex3d 5892 opabex3 5893 enq0ref 6992 setindis 11862 bdsetindis 11864 |
Copyright terms: Public domain | W3C validator |