![]() |
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 2087 | . 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 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1842 |
This theorem is referenced by: equtr 2091 equeuclr 2093 stdpc7 2099 spfw 2104 spfwOLD 2105 cbvalw 2107 alcomiw 2110 ax8 2133 elequ1 2134 ax9 2140 elequ2 2141 sbequ12r 2247 cbvalv1 2308 cbval 2404 cbvalv 2406 sbequ 2501 sb9 2551 reu8 3531 sbcco2 3588 reu8nf 3645 opeliunxp 5315 elrnmpt1 5517 fvn0ssdmfun 6501 elabrex 6652 snnexOLD 7120 tfisi 7211 tfinds2 7216 opabex3d 7298 opabex3 7299 mpt2curryd 7552 boxriin 8104 ixpiunwdom 8649 elirrv 8654 rabssnn0fi 12950 fproddivf 14888 prmodvdslcmf 15924 imasvscafn 16370 1mavmul 20527 ptbasfi 21557 elmptrab 21803 pcoass 22995 iundisj2 23488 dchrisumlema 25347 dchrisumlem2 25349 cusgrfilem2 26533 frgrncvvdeq 27434 frgr2wwlk1 27454 iundisj2f 29681 iundisj2fi 29836 bnj1014 31308 cvmsss2 31534 ax8dfeq 31980 bj-ssbid1ALT 32925 bj-cbvexw 32941 bj-sb 32954 bj-cleljustab 33124 bj-ax9-2 33168 finxpreclem6 33515 wl-nfs1t 33606 wl-equsb4 33620 wl-euequ1f 33638 wl-ax11-lem8 33651 wl-ax8clv1 33660 wl-clelv2-just 33661 matunitlindflem1 33687 poimirlem26 33717 mblfinlem2 33729 sdclem2 33820 axc11-o 34709 rexzrexnn0 37839 elabrexg 39674 disjinfi 39848 dvnmptdivc 40625 iblsplitf 40658 vonn0ioo2 41379 vonn0icc2 41381 uspgrsprf1 42234 opeliun2xp 42590 |
Copyright terms: Public domain | W3C validator |