**Description:** A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018)

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

Assertion | eqneqall | $${\u22a2}{A}={B}\to \left({A}\ne {B}\to {\phi}\right)$$ |

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

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

2 | pm2.24 | $${\u22a2}{A}={B}\to \left(\neg {A}={B}\to {\phi}\right)$$ | |

3 | 1 2 | syl5bi | $${\u22a2}{A}={B}\to \left({A}\ne {B}\to {\phi}\right)$$ |