![]() |
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 2744 | . 2 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) |
3 | 2 | necon3bid 2985 | 1 ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ≠ wne 2940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 df-ne 2941 |
This theorem is referenced by: neeq2 3004 neeqtrd 3010 prneprprc 4819 fndifnfp 7123 f12dfv 7220 f13dfv 7221 infpssrlem4 10247 sqrt2irr 16136 dsmmval 21156 dsmmbas2 21159 frlmbas 21177 dfconn2 22786 alexsublem 23411 uc1pval 25520 mon1pval 25522 dchrsum2 26632 noetainflem4 27104 isinag 27822 uhgrwkspthlem2 28744 usgr2wlkneq 28746 usgr2trlspth 28751 lfgrn1cycl 28792 uspgrn2crct 28795 2pthdlem1 28917 3pthdlem1 29150 numclwwlk2lem1 29362 eigorth 30822 eighmorth 30948 prmidlval 32257 mxidlval 32278 ressply1mon1p 32327 wlimeq12 34450 limsucncmpi 34963 poimirlem25 36149 poimirlem26 36150 pridlval 36538 maxidlval 36544 lshpset 37486 lduallkr3 37670 isatl 37807 cdlemk42 39450 sdrgunit 40760 prjspner1 41007 dffltz 41015 stoweidlem43 44370 nnfoctbdjlem 44782 |
Copyright terms: Public domain | W3C validator |