![]() |
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 2102 | . 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 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 |
This theorem is referenced by: equtr 2106 equeuclr 2108 stdpc7 2114 spfw 2121 spfwOLD 2122 cbvalw 2124 alcomiw 2127 alcomiwOLD 2128 ax8 2151 elequ1 2152 ax9 2158 elequ2 2159 sbequ12r 2268 cbvalv1 2336 cbval 2432 cbvalv 2434 sbequ 2523 sb9 2573 rabrabi 3350 reu8 3555 sbcco2 3612 reu8nf 3666 opeliunxp 5311 elrnmpt1 5513 fvn0ssdmfun 6494 elabrex 6645 snnexOLD 7115 tfisi 7206 tfinds2 7211 opabex3d 7293 opabex3 7294 mpt2curryd 7548 boxriin 8105 ixpiunwdom 8653 elirrv 8658 rabssnn0fi 12994 fproddivf 14925 prmodvdslcmf 15959 1mavmul 20573 ptbasfi 21606 elmptrab 21852 pcoass 23044 iundisj2 23538 dchrisumlema 25399 dchrisumlem2 25401 cusgrfilem2 26588 frgrncvvdeq 27492 frgr2wwlk1 27512 iundisj2f 29742 iundisj2fi 29897 bnj1014 31369 cvmsss2 31595 ax8dfeq 32041 bj-ssbid1ALT 32986 bj-cbvexw 33002 bj-sb 33015 bj-cleljustab 33182 bj-ax9-2 33221 finxpreclem6 33571 wl-nfs1t 33660 wl-equsb4 33674 wl-euequ1f 33691 wl-ax11-lem8 33704 wl-ax8clv1 33712 wl-clelv2-just 33713 matunitlindflem1 33739 poimirlem26 33769 mblfinlem2 33781 sdclem2 33871 axc11-o 34760 rexzrexnn0 37895 elabrexg 39729 disjinfi 39901 dvnmptdivc 40672 iblsplitf 40704 vonn0ioo2 41425 vonn0icc2 41427 uspgrsprf1 42284 opeliun2xp 42640 |
Copyright terms: Public domain | W3C validator |