Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neeqtrd | Structured version Visualization version GIF 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 2842 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶)) |
4 | 1, 3 | mpbid 221 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ≠ wne 2780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 df-ne 2782 |
This theorem is referenced by: neeqtrrd 2856 3netr3d 2858 xaddass2 11952 xov1plusxeqvd 12189 issubdrg 18628 ply1scln0 19482 qsssubdrg 19624 alexsublem 21658 cphsubrglem 22785 cphreccllem 22786 mdegldg 23630 tglinethru 25331 footex 25413 eupath2lem3 26506 poimirlem26 32605 lkrpssN 33468 lnatexN 34083 lhpexle2lem 34313 lhpexle3lem 34315 cdlemg47 35042 cdlemk54 35264 tendoinvcl 35411 lcdlkreqN 35929 mapdh8ab 36084 jm2.26lem3 36586 stoweidlem36 38929 |
Copyright terms: Public domain | W3C validator |