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 3076 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶)) |
4 | 1, 3 | mpbid 233 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: neeqtrrd 3090 3netr3d 3092 xaddass2 12633 xov1plusxeqvd 12874 ablsimpgfindlem1 19160 issubdrg 19491 ply1scln0 20389 qsssubdrg 20534 alexsublem 22582 cphsubrglem 23710 cphreccllem 23711 mdegldg 24589 tglinethru 26350 footexALT 26432 footexlem2 26434 poimirlem26 34800 lkrpssN 36181 lnatexN 36797 lhpexle2lem 37027 lhpexle3lem 37029 cdlemg47 37754 cdlemk54 37976 tendoinvcl 38122 lcdlkreqN 38640 mapdh8ab 38795 jm2.26lem3 39478 stoweidlem36 42202 smndex2dnrinv 43985 |
Copyright terms: Public domain | W3C validator |