![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equcoms | Structured version Visualization version Unicode version |
Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.) |
Ref | Expression |
---|---|
equcoms.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
equcoms |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcomi 1861 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equcoms.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 |
This theorem is referenced by: equtr 1865 equtr2 1869 stdpc7 1871 ax13b 1874 spfw 1875 cbvalw 1877 alcomiw 1880 elequ1 1894 elequ2 1901 19.8a 1935 19.8aOLD 1936 cbvalv1 2064 sbequ12r 2084 cbval 2114 sbequ 2205 sb9 2255 euequ1 2305 reu8 3234 sbcco2 3291 opeliunxp 4886 elrnmpt1 5083 iotaval 5557 fvn0ssdmfun 6013 elabrex 6148 snnex 6597 tfisi 6685 tfinds2 6690 opabex3d 6771 opabex3 6772 mpt2curryd 7016 boxriin 7564 ixpiunwdom 8106 elirrv 8112 rabssnn0fi 12198 fproddivf 14041 prmodvdslcmf 15005 prmordvdslcmfOLD 15019 prmordvdslcmsOLDOLD 15021 imasvscafn 15443 1mavmul 19573 ptbasfi 20596 elmptrab 20842 pcoass 22055 iundisj2 22502 dchrisumlema 24326 dchrisumlem2 24328 cusgrafilem2 25208 frgrancvvdeqlem9 25769 iundisj2f 28200 iundisj2fi 28373 bnj1014 29771 cvmsss2 29997 ax8dfeq 30445 bj-ssbid1ALT 31261 bj-cbvexw 31273 finxpreclem6 31788 wl-nfs1t 31871 wl-equsb4 31885 wl-euequ1f 31903 wl-19.8a 31910 wl-ax11-lem8 31922 poimirlem26 31966 mblfinlem2 31978 sdclem2 32071 ax13fromc9 32476 axc11-o 32522 rexzrexnn0 35647 elabrexg 37370 disjinfi 37468 iblsplitf 37847 cusgrfilem2 39517 opeliun2xp 40167 |
Copyright terms: Public domain | W3C validator |