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 225 | . . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑) |
3 | 2 | necon3abii 3062 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
4 | 3 | bicomi 225 | 1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: necon1abii 3064 nssinpss 4232 difsnpss 4734 xpdifid 6019 wfi 6175 ordintdif 6234 tfi 7556 oelim2 8211 0sdomg 8635 fin23lem26 9736 axdc3lem4 9864 axdc4lem 9866 axcclem 9868 crreczi 13579 ef0lem 15422 lidlnz 19931 nconnsubb 21961 ufileu 22457 itg2cnlem1 24291 plyeq0lem 24729 abelthlem2 24949 ppinprm 25657 chtnprm 25659 ltgov 26311 usgr2pthlem 27472 shne0i 29153 pjneli 29428 eleigvec 29662 nmo 30182 qqhval2lem 31122 qqhval2 31123 sibfof 31498 dffr5 32887 frpoind 32978 frind 32983 ellimits 33269 elicc3 33563 itg2addnclem2 34826 ftc1anclem3 34851 onfrALTlem5 40756 onfrALTlem5VD 41099 limcrecl 41790 |
Copyright terms: Public domain | W3C validator |