Metamath Proof Explorer


Theorem eqneqall

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

Ref Expression
Assertion eqneqall A = B A B φ

Proof

Step Hyp Ref Expression
1 df-ne A B ¬ A = B
2 pm2.24 A = B ¬ A = B φ
3 1 2 syl5bi A = B A B φ