![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3bbii | Structured version Visualization version GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.) |
Ref | Expression |
---|---|
necon3bbii.1 | ⊢ (𝜑 ↔ 𝐴 = 𝐵) |
Ref | Expression |
---|---|
necon3bbii | ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3bbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝐴 = 𝐵) | |
2 | 1 | bicomi 214 | . . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑) |
3 | 2 | necon3abii 2978 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
4 | 3 | bicomi 214 | 1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 = wceq 1632 ≠ wne 2932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-ne 2933 |
This theorem is referenced by: necon1abii 2980 nssinpss 3999 difsnpss 4483 xpdifid 5720 wfi 5874 ordintdif 5935 tfi 7218 oelim2 7844 0sdomg 8254 fin23lem26 9339 axdc3lem4 9467 axdc4lem 9469 axcclem 9471 crreczi 13183 ef0lem 15008 lidlnz 19430 nconnsubb 21428 ufileu 21924 itg2cnlem1 23727 plyeq0lem 24165 abelthlem2 24385 ppinprm 25077 chtnprm 25079 ltgov 25691 usgr2pthlem 26869 shne0i 28616 pjneli 28891 eleigvec 29125 nmo 29634 qqhval2lem 30334 qqhval2 30335 sibfof 30711 dffr5 31950 frpoind 32046 frind 32049 ellimits 32323 elicc3 32617 itg2addnclem2 33775 ftc1anclem3 33800 onfrALTlem5 39259 onfrALTlem5VD 39620 limcrecl 40364 |
Copyright terms: Public domain | W3C validator |