![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neeqtrd | Structured version Visualization version Unicode version |
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
Ref | Expression |
---|---|
neeqtrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
neeqtrd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
neeqtrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeqtrd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | neeqtrd.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | neeq2d 2684 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbid 214 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-cleq 2444 df-ne 2624 |
This theorem is referenced by: neeqtrrd 2698 3netr3d 2700 xaddass2 11536 xov1plusxeqvd 11778 issubdrg 18033 ply1scln0 18884 qsssubdrg 19027 alexsublem 21059 cphsubrglem 22155 cphreccllem 22156 mdegldg 23015 tglinethru 24681 footex 24763 eupath2lem3 25707 poimirlem26 31966 lkrpssN 32729 lnatexN 33344 lhpexle2lem 33574 lhpexle3lem 33576 cdlemg47 34303 cdlemk54 34525 tendoinvcl 34672 lcdlkreqN 35190 mapdh8ab 35345 jm2.26lem3 35856 stoweidlem36 37897 |
Copyright terms: Public domain | W3C validator |