![]() |
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 2991 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶)) |
4 | 1, 3 | mpbid 231 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ≠ wne 2930 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ne 2931 |
This theorem is referenced by: neeqtrrd 3005 3netr3d 3007 xaddass2 13283 xov1plusxeqvd 13529 smndex2dnrinv 18905 ablsimpgfindlem1 20107 issubdrg 20759 qsssubdrg 21423 ply1scln0 22283 alexsublem 24039 cphsubrglem 25196 cphreccllem 25197 mdegldg 26093 nosep2o 27712 noetainflem4 27770 tglinethru 28563 footexALT 28645 footexlem2 28647 nrt2irr 30406 sdrgdvcl 33149 sdrginvcl 33150 0ringprmidl 33324 0ringmon1p 33430 irngnzply1lem 33566 irngnminplynz 33581 minplym1p 33582 algextdeglem4 33587 poimirlem26 37347 lkrpssN 38861 lnatexN 39478 lhpexle2lem 39708 lhpexle3lem 39710 cdlemg47 40435 cdlemk54 40657 tendoinvcl 40803 lcdlkreqN 41321 mapdh8ab 41476 aks6d1c5lem2 41836 aks6d1c7 41882 jm2.26lem3 42659 stoweidlem36 45657 |
Copyright terms: Public domain | W3C validator |