![]() |
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 2064 | . 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 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 |
This theorem is referenced by: equtr 2068 equeuclr 2070 stdpc7 2076 spfw 2083 cbvalw 2085 alcomiw 2088 alcomiwOLD 2089 ax8 2113 elequ1 2114 ax9 2120 elequ2 2121 sbequ12r 2230 sbequvv 2288 cbvalv1 2312 cbval 2368 cbvalv 2370 sbequ 2452 sb9 2503 rabrabi 3397 reu8 3614 sbcco2 3676 reu8nf 3733 opeliunxp 5418 elrnmpt1 5622 elidinxp 5707 fvn0ssdmfun 6616 elabrex 6775 tfisi 7338 tfinds2 7343 opabex3d 7425 opabex3 7426 mpt2curryd 7679 boxriin 8238 ixpiunwdom 8787 elirrv 8792 rabssnn0fi 13108 fproddivf 15124 prmodvdslcmf 16159 1mavmul 20763 ptbasfi 21797 elmptrab 22043 pcoass 23235 iundisj2 23757 dchrisumlema 25633 dchrisumlem2 25635 cusgrfilem2 26808 frgrncvvdeq 27721 frgr2wwlk1 27741 iundisj2f 29970 iundisj2fi 30124 bnj1014 31633 cvmsss2 31859 ax8dfeq 32296 bj-ssbid1ALT 33242 bj-cbvexw 33257 bj-sb 33270 bj-cleljustab 33426 bj-ax9-2 33466 finxpreclem6 33831 wl-nfs1t 33921 wl-equsb4 33936 wl-euequf 33953 wl-ax11-lem8 33966 wl-ax8clv1 34008 wl-clelv2-just 34009 matunitlindflem1 34036 poimirlem26 34066 mblfinlem2 34078 sdclem2 34167 axc11-o 35110 rexzrexnn0 38338 elabrexg 40149 disjinfi 40313 dvnmptdivc 41091 iblsplitf 41123 vonn0ioo2 41841 vonn0icc2 41843 funressnvmo 42119 funressnvmoOLD 42120 paireqne 42460 uspgrsprf1 42780 opeliun2xp 43136 |
Copyright terms: Public domain | W3C validator |