![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equcoms | Structured version Visualization version GIF 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 2012 | . 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦) | |
2 | equcoms.1 | . 2 ⊢ (𝑥 = 𝑦 → 𝜑) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝑦 = 𝑥 → 𝜑) |
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 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 |
This theorem is referenced by: equtr 2016 equeuclr 2018 spfw 2028 cbvalw 2030 alcomiw 2038 ax8 2104 elequ1 2105 ax9 2112 elequ2 2113 stdpc7 2237 sbequ12r 2239 cbvalv1 2331 cbval 2391 sb9 2512 ax9ALT 2720 sbralieALT 3342 rabrabi 3437 reurab 3694 reu8 3726 sbcco2 3802 reu8nf 3869 notabw 4304 ab0OLD 4379 sbcop1 5493 opeliunxp 5748 elrnmpt1 5963 elidinxp 6052 fvn0ssdmfun 7087 elabrex 7256 elabrexg 7257 riotarab 7422 tfisi 7868 tfinds2 7873 opabex3d 7978 opabex3rd 7979 opabex3 7980 xpord2indlem 8160 xpord3inddlem 8167 mpocurryd 8283 boxriin 8968 ixpiunwdom 9629 elirrv 9635 rabssnn0fi 14001 fproddivf 15984 prmodvdslcmf 17044 eqg0subg 19185 1mavmul 22533 ptbasfi 23568 elmptrab 23814 pcoass 25034 iundisj2 25561 dchrisumlema 27509 dchrisumlem2 27511 cusgrfilem2 29385 frgrncvvdeq 30234 frgr2wwlk1 30254 iundisj2f 32501 iundisj2fi 32688 bnj1014 34762 cvmsss2 35054 gonarlem 35174 ax8dfeq 35570 bj-ssbid1ALT 36317 bj-cbvexw 36328 bj-sb 36340 finxpreclem6 37051 ralssiun 37062 wl-nfs1t 37180 wl-equsb4 37200 wl-euequf 37217 wl-ax11-lem8 37235 matunitlindflem1 37265 poimirlem26 37295 mblfinlem2 37307 sdclem2 37391 axc11-o 38597 evl1gprodd 41763 idomnnzgmulnz 41779 abbibw 42269 rexzrexnn0 42398 disjinfi 44736 dvnmptdivc 45496 iblsplitf 45528 vonn0ioo2 46248 vonn0icc2 46250 funressnvmo 46597 ichcircshi 46963 ichreuopeq 46982 paireqne 47020 reuopreuprim 47035 uspgrsprf1 47461 opeliun2xp 47648 |
Copyright terms: Public domain | W3C validator |