Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neeq2d | Structured version Visualization version GIF version |
Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
Ref | Expression |
---|---|
neeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
neeq2d | ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | eqeq2d 2832 | . 2 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) |
3 | 2 | necon3bid 3060 | 1 ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = 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: neeq2 3079 neeqtrd 3085 prneprprc 4785 fndifnfp 6931 f12dfv 7021 f13dfv 7022 infpssrlem4 9717 sqrt2irr 15592 dsmmval 20808 dsmmbas2 20811 frlmbas 20829 dfconn2 21957 alexsublem 22582 uc1pval 24662 mon1pval 24664 dchrsum2 25772 isinag 26552 uhgrwkspthlem2 27463 usgr2wlkneq 27465 usgr2trlspth 27470 lfgrn1cycl 27511 uspgrn2crct 27514 2pthdlem1 27637 3pthdlem1 27871 numclwwlk2lem1 28083 eigorth 29543 eighmorth 29669 prmidlval 30874 wlimeq12 33004 limsucncmpi 33691 poimirlem25 34799 poimirlem26 34800 pridlval 35194 maxidlval 35200 lshpset 35996 lduallkr3 36180 isatl 36317 cdlemk42 37959 dffltz 39151 stoweidlem43 42209 nnfoctbdjlem 42618 |
Copyright terms: Public domain | W3C validator |