Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007) (Proof shortened by Andrew Salmon, 25-May-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pm2.61dne.1 | |- ( ph -> ( A = B -> ps ) ) |
|
pm2.61dne.2 | |- ( ph -> ( A =/= B -> ps ) ) |
||
Assertion | pm2.61dne | |- ( ph -> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61dne.1 | |- ( ph -> ( A = B -> ps ) ) |
|
2 | pm2.61dne.2 | |- ( ph -> ( A =/= B -> ps ) ) |
|
3 | nne | |- ( -. A =/= B <-> A = B ) |
|
4 | 3 1 | syl5bi | |- ( ph -> ( -. A =/= B -> ps ) ) |
5 | 2 4 | pm2.61d | |- ( ph -> ps ) |