| 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 2016 | . 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 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: equtr 2020 equeuclr 2022 spfw 2032 cbvalw 2034 alcomimw 2042 ax8 2114 elequ1 2115 ax9 2122 elequ2 2123 stdpc7 2250 sbequ12r 2252 cbvalv1 2343 cbval 2403 sb9 2524 ax9ALT 2732 sbralieALT 3359 rabrabi 3456 reurab 3707 reu8 3739 sbcco2 3815 reu8nf 3877 notabw 4313 sbcop1 5493 opeliunxp 5752 opeliun2xp 5753 elrnmpt1 5971 elidinxp 6062 fvn0ssdmfun 7094 elabrex 7262 elabrexg 7263 riotarab 7430 tfisi 7880 tfinds2 7885 opabex3d 7990 opabex3rd 7991 opabex3 7992 xpord2indlem 8172 xpord3inddlem 8179 mpocurryd 8294 boxriin 8980 ixpiunwdom 9630 elirrv 9636 rabssnn0fi 14027 fproddivf 16023 prmodvdslcmf 17085 eqg0subg 19214 1mavmul 22554 ptbasfi 23589 elmptrab 23835 pcoass 25057 iundisj2 25584 dchrisumlema 27532 dchrisumlem2 27534 cusgrfilem2 29474 frgrncvvdeq 30328 frgr2wwlk1 30348 iundisj2f 32603 iundisj2fi 32799 bnj1014 34975 cvmsss2 35279 gonarlem 35399 ax8dfeq 35799 in-ax8 36225 ss-ax8 36226 bj-ssbid1ALT 36666 bj-cbvexw 36677 bj-sb 36688 finxpreclem6 37397 ralssiun 37408 wl-nfs1t 37538 wl-equsb4 37558 wl-euequf 37575 wl-ax11-lem8 37593 matunitlindflem1 37623 poimirlem26 37653 mblfinlem2 37665 sdclem2 37749 axc11-o 38952 evl1gprodd 42118 idomnnzgmulnz 42134 abbibw 42687 rexzrexnn0 42815 disjinfi 45197 dvnmptdivc 45953 iblsplitf 45985 vonn0ioo2 46705 vonn0icc2 46707 funressnvmo 47057 ichcircshi 47441 ichreuopeq 47460 paireqne 47498 reuopreuprim 47513 uspgrsprf1 48063 |
| Copyright terms: Public domain | W3C validator |