| 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 3010 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐷) |
| 5 | 1, 4 | eqnetrrd 3009 | 1 ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ≠ wne 2940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ne 2941 |
| This theorem is referenced by: subrgnzr 20594 clmopfne 25129 dchrisum0re 27557 fracfld 33310 qsnzr 33483 dimlssid 33683 algextdeglem4 33761 constrrtll 33772 cdlemg9a 40634 cdlemg11aq 40640 cdlemg12b 40646 cdlemg12 40652 cdlemg13 40654 cdlemg19 40686 cdlemk3 40835 cdlemk12 40852 cdlemk12u 40874 lclkrlem2g 41515 mapdncol 41672 mapdpglem29 41702 hdmaprnlem1N 41851 hdmap14lem9 41878 aks6d1c2p2 42120 ricdrng1 42538 pellex 42846 |
| Copyright terms: Public domain | W3C validator |