Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3netr4d | 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, 21-Nov-2019.) |
Ref | Expression |
---|---|
3netr4d.1 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
3netr4d.2 | ⊢ (𝜑 → 𝐶 = 𝐴) |
3netr4d.3 | ⊢ (𝜑 → 𝐷 = 𝐵) |
Ref | Expression |
---|---|
3netr4d | ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3netr4d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐴) | |
2 | 3netr4d.1 | . . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
3 | 1, 2 | eqnetrd 3083 | . 2 ⊢ (𝜑 → 𝐶 ≠ 𝐵) |
4 | 3netr4d.3 | . 2 ⊢ (𝜑 → 𝐷 = 𝐵) | |
5 | 3, 4 | neeqtrrd 3090 | 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: infpssrlem4 9717 modsumfzodifsn 13302 mgm2nsgrplem4 18026 pmtr3ncomlem1 18532 isdrng2 19443 prmirredlem 20570 uvcf1 20866 dfac14lem 22155 i1fmullem 24224 fta1glem1 24688 fta1blem 24691 plydivlem4 24814 fta1lem 24825 cubic 25354 asinlem 25373 dchrn0 25754 lgsne0 25839 perpneq 26428 axlowdimlem14 26669 preimane 30344 cycpmco2lem6 30701 cycpmrn 30713 cntnevol 31387 subfacp1lem5 32329 noextenddif 33073 noresle 33098 fvtransport 33391 poimirlem1 34775 poimirlem6 34780 poimirlem7 34781 dalem4 36683 cdleme35sn2aw 37476 cdleme39n 37484 cdleme41fva11 37495 trlcone 37746 hdmaprnlem3N 38868 uvcn0 39031 stoweidlem23 42189 2zrngnmlid 44118 2zrngnmrid 44119 zlmodzxznm 44450 line2y 44640 |
Copyright terms: Public domain | W3C validator |