**Description:** Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011)

Ref | Expression | ||
---|---|---|---|

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

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

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

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

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

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

3 | 1 | ex | $${\u22a2}{\phi}\to \left({A}={B}\to {\psi}\right)$$ |

4 | 2 | ex | $${\u22a2}{\phi}\to \left({A}\ne {B}\to {\psi}\right)$$ |

5 | 3 4 | pm2.61dne | $${\u22a2}{\phi}\to {\psi}$$ |