**Description:** Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006)

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

Hypothesis | necon3d.1 | $${\u22a2}{\phi}\to \left({A}={B}\to {C}={D}\right)$$ | |

Assertion | necon3d | $${\u22a2}{\phi}\to \left({C}\ne {D}\to {A}\ne {B}\right)$$ |

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

1 | necon3d.1 | $${\u22a2}{\phi}\to \left({A}={B}\to {C}={D}\right)$$ | |

2 | 1 | necon3ad | $${\u22a2}{\phi}\to \left({C}\ne {D}\to \neg {A}={B}\right)$$ |

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

4 | 2 3 | syl6ibr | $${\u22a2}{\phi}\to \left({C}\ne {D}\to {A}\ne {B}\right)$$ |