**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 | $${\u22a2}{\phi}\to \left({A}={B}\to {\psi}\right)$$ | |

pm2.61dne.2 | $${\u22a2}{\phi}\to \left({A}\ne {B}\to {\psi}\right)$$ | ||

Assertion | pm2.61dne | $${\u22a2}{\phi}\to {\psi}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | pm2.61dne.1 | $${\u22a2}{\phi}\to \left({A}={B}\to {\psi}\right)$$ | |

2 | pm2.61dne.2 | $${\u22a2}{\phi}\to \left({A}\ne {B}\to {\psi}\right)$$ | |

3 | nne | $${\u22a2}\neg {A}\ne {B}\leftrightarrow {A}={B}$$ | |

4 | 3 1 | syl5bi | $${\u22a2}{\phi}\to \left(\neg {A}\ne {B}\to {\psi}\right)$$ |

5 | 2 4 | pm2.61d | $${\u22a2}{\phi}\to {\psi}$$ |