| 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 224 | . . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑) |
| 3 | 2 | necon3abii 2987 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
| 4 | 3 | bicomi 224 | 1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 = wceq 1540 ≠ wne 2940 |
| 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 207 df-ne 2941 |
| This theorem is referenced by: necon1abii 2989 nssinpss 4267 difsnpss 4807 xpdifid 6188 frpoind 6363 wfiOLD 6372 ordintdif 6434 tfi 7874 oelim2 8633 0sdomg 9144 0sdomgOLD 9145 frind 9790 fin23lem26 10365 axdc3lem4 10493 axdc4lem 10495 axcclem 10497 crreczi 14267 ef0lem 16114 lidlnz 21252 nconnsubb 23431 ufileu 23927 itg2cnlem1 25796 plyeq0lem 26249 abelthlem2 26476 ppinprm 27195 chtnprm 27197 sltlpss 27945 mulsval 28135 ltgov 28605 usgr2pthlem 29783 shne0i 31467 pjneli 31742 eleigvec 31976 nmo 32509 qqhval2lem 33982 qqhval2 33983 sibfof 34342 dffr5 35754 ellimits 35911 elicc3 36318 itg2addnclem2 37679 ftc1anclem3 37702 onfrALTlem5 44562 onfrALTlem5VD 44905 limcrecl 45644 dfnbgr6 47843 |
| Copyright terms: Public domain | W3C validator |