Theorem eqneqall 2430

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 2421	. 2 |- ( A =/= B <-> -. A = B )
2		pm2.24 630	. 2 |- ( A = B -> ( -. A = B -> ph ) )
3	1, 2	biimtrid 152	1 |- ( A = B -> ( A =/= B -> ph ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in2 624

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  ssprsseq  3877  eldju2ndl  7418  eldju2ndr  7419  modfzo0difsn  10853  nno  12698  prm2orodd  12929  prm23lt5  13071  dvdsprmpweqnn  13144  logbgcd1irr  16203  gausslemma2dlem0f  16378  gausslemma2dlem0i  16381  2lgs  16428  2lgsoddprm  16437  umgrnloop2  16597  uhgr2edg  16652  umgrclwwlkge2  16848