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 213 | . . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑) |
3 | 2 | necon3abii 2828 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
4 | 3 | bicomi 213 | 1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 = wceq 1475 ≠ wne 2780 |
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 196 df-ne 2782 |
This theorem is referenced by: necon1abii 2830 nssinpss 3818 difsnpss 4279 xpdifid 5481 wfi 5630 ordintdif 5691 tfi 6945 oelim2 7562 0sdomg 7974 fin23lem26 9030 axdc3lem4 9158 axdc4lem 9160 axcclem 9162 crreczi 12851 ef0lem 14648 lidlnz 19049 nconsubb 21036 ufileu 21533 itg2cnlem1 23334 plyeq0lem 23770 abelthlem2 23990 ppinprm 24678 chtnprm 24680 ltgov 25292 shne0i 27691 pjneli 27966 eleigvec 28200 nmo 28709 qqhval2lem 29353 qqhval2 29354 sibfof 29729 dffr5 30896 frind 30984 ellimits 31187 elicc3 31481 itg2addnclem2 32632 ftc1anclem3 32657 onfrALTlem5 37778 limcrecl 38696 usgr2pthlem 40969 |
Copyright terms: Public domain | W3C validator |