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 3085 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐷) |
5 | 1, 4 | eqnetrrd 3084 | 1 ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: subrgnzr 19971 clmopfne 23629 dchrisum0re 26017 cdlemg9a 37650 cdlemg11aq 37656 cdlemg12b 37662 cdlemg12 37668 cdlemg13 37670 cdlemg19 37702 cdlemk3 37851 cdlemk12 37868 cdlemk12u 37890 lclkrlem2g 38531 mapdncol 38688 mapdpglem29 38718 hdmaprnlem1N 38867 hdmap14lem9 38894 pellex 39312 |
Copyright terms: Public domain | W3C validator |