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 2854 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶)) |
4 | 1, 3 | mpbid 222 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: neeqtrrd 2868 3netr3d 2870 xaddass2 12080 xov1plusxeqvd 12318 issubdrg 18805 ply1scln0 19661 qsssubdrg 19805 alexsublem 21848 cphsubrglem 22977 cphreccllem 22978 mdegldg 23826 tglinethru 25531 footex 25613 poimirlem26 33435 lkrpssN 34450 lnatexN 35065 lhpexle2lem 35295 lhpexle3lem 35297 cdlemg47 36024 cdlemk54 36246 tendoinvcl 36393 lcdlkreqN 36911 mapdh8ab 37066 jm2.26lem3 37568 stoweidlem36 40253 |
Copyright terms: Public domain | W3C validator |