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 -> ph ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( A =/= B <-> -. A = B )
2 pm2.24 
 |-  ( A = B -> ( -. A = B -> ph ) )
3 1 2 syl5bi 
 |-  ( A = B -> ( A =/= B -> ph ) )