Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007)
Ref | Expression | ||
---|---|---|---|
Hypothesis | necon3abid.1 | |- ( ph -> ( A = B <-> ps ) ) |
|
Assertion | necon3abid | |- ( ph -> ( A =/= B <-> -. ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3abid.1 | |- ( ph -> ( A = B <-> ps ) ) |
|
2 | df-ne | |- ( A =/= B <-> -. A = B ) |
|
3 | 1 | notbid | |- ( ph -> ( -. A = B <-> -. ps ) ) |
4 | 2 3 | bitrid | |- ( ph -> ( A =/= B <-> -. ps ) ) |