![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3netr3d | Structured version Visualization version GIF version |
Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
Ref | Expression |
---|---|
3netr3d.1 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
3netr3d.2 | ⊢ (𝜑 → 𝐴 = 𝐶) |
3netr3d.3 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
3netr3d | ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3netr3d.2 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) | |
2 | 3netr3d.1 | . . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
3 | 3netr3d.3 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐷) | |
4 | 2, 3 | neeqtrd 3008 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐷) |
5 | 1, 4 | eqnetrrd 3007 | 1 ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ≠ wne 2938 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-ne 2939 |
This theorem is referenced by: subrgnzr 20611 clmopfne 25143 dchrisum0re 27572 fracfld 33290 qsnzr 33463 dimlssid 33660 algextdeglem4 33726 constrrtll 33737 cdlemg9a 40615 cdlemg11aq 40621 cdlemg12b 40627 cdlemg12 40633 cdlemg13 40635 cdlemg19 40667 cdlemk3 40816 cdlemk12 40833 cdlemk12u 40855 lclkrlem2g 41496 mapdncol 41653 mapdpglem29 41683 hdmaprnlem1N 41832 hdmap14lem9 41859 aks6d1c2p2 42101 ricdrng1 42515 pellex 42823 |
Copyright terms: Public domain | W3C validator |