Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 25-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pm2.61ne.1 | |- ( A = B -> ( ps <-> ch ) ) |
|
pm2.61ne.2 | |- ( ( ph /\ A =/= B ) -> ps ) |
||
pm2.61ne.3 | |- ( ph -> ch ) |
||
Assertion | pm2.61ne | |- ( ph -> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61ne.1 | |- ( A = B -> ( ps <-> ch ) ) |
|
2 | pm2.61ne.2 | |- ( ( ph /\ A =/= B ) -> ps ) |
|
3 | pm2.61ne.3 | |- ( ph -> ch ) |
|
4 | 3 1 | syl5ibr | |- ( A = B -> ( ph -> ps ) ) |
5 | 2 | expcom | |- ( A =/= B -> ( ph -> ps ) ) |
6 | 4 5 | pm2.61ine | |- ( ph -> ps ) |