**Description:** Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005) (Proof shortened by Andrew Salmon, 25-May-2011)

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

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

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

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

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

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

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

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