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  7413  eldju2ndr  7414  modfzo0difsn  10847  nno  12692  prm2orodd  12923  prm23lt5  13065  dvdsprmpweqnn  13138  logbgcd1irr  16164  gausslemma2dlem0f  16339  gausslemma2dlem0i  16342  2lgs  16389  2lgsoddprm  16398  umgrnloop2  16558  uhgr2edg  16613  umgrclwwlkge2  16809