![]() |
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 3046 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶)) |
4 | 1, 3 | mpbid 233 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1525 ≠ wne 2986 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-9 2093 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1766 df-cleq 2790 df-ne 2987 |
This theorem is referenced by: neeqtrrd 3060 3netr3d 3062 xaddass2 12497 xov1plusxeqvd 12738 issubdrg 19254 ply1scln0 20146 qsssubdrg 20290 alexsublem 22340 cphsubrglem 23468 cphreccllem 23469 mdegldg 24347 tglinethru 26108 footexALT 26190 footexlem2 26192 poimirlem26 34470 lkrpssN 35851 lnatexN 36467 lhpexle2lem 36697 lhpexle3lem 36699 cdlemg47 37424 cdlemk54 37646 tendoinvcl 37792 lcdlkreqN 38310 mapdh8ab 38465 jm2.26lem3 39104 ablsimpgfindlem1 40186 stoweidlem36 41885 |
Copyright terms: Public domain | W3C validator |