Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neeqtrri | Structured version Visualization version Unicode version |
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
Ref | Expression |
---|---|
neeqtrr.1 | |
neeqtrr.2 |
Ref | Expression |
---|---|
neeqtrri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeqtrr.1 | . 2 | |
2 | neeqtrr.2 | . . 3 | |
3 | 2 | eqcomi 2631 | . 2 |
4 | 1, 3 | neeqtri 2866 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 wne 2794 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-ne 2795 |
This theorem is referenced by: cflim2 9085 pnfnemnf 10094 resslem 15933 basendxnplusgndx 15989 plusgndxnmulrndx 15998 basendxnmulrndx 15999 slotsbhcdif 16080 rmodislmod 18931 cnfldfun 19758 xrsnsgrp 19782 zlmlem 19865 matbas 20219 matplusg 20220 matvsca 20222 tnglem 22444 setsvtx 25927 resvlem 29831 limsucncmpi 32444 |
Copyright terms: Public domain | W3C validator |