Theorem eqneqall 2424

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

Assertion

Ref	Expression
eqneqall	|- ( A = B -> ( A =/= B -> ph ) )

Proof of Theorem eqneqall

Step	Hyp	Ref	Expression
1		df-ne 2415	. 2 |- ( A =/= B <-> -. A = B )
2		pm2.24 626	. 2 |- ( A = B -> ( -. A = B -> ph ) )
3	1, 2	biimtrid 152	1 |- ( A = B -> ( A =/= B -> ph ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in2 620

This theorem depends on definitions:  df-bi 117  df-ne 2415

This theorem is referenced by:  ssprsseq  3861  eldju2ndl  7376  eldju2ndr  7377  modfzo0difsn  10781  nno  12617  prm2orodd  12848  prm23lt5  12986  dvdsprmpweqnn  13059  logbgcd1irr  15958  gausslemma2dlem0f  16053  gausslemma2dlem0i  16056  2lgs  16103  2lgsoddprm  16112  umgrnloop2  16272  uhgr2edg  16327  umgrclwwlkge2  16523