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  7412  eldju2ndr  7413  modfzo0difsn  10845  nno  12689  prm2orodd  12920  prm23lt5  13062  dvdsprmpweqnn  13135  logbgcd1irr  16122  gausslemma2dlem0f  16271  gausslemma2dlem0i  16274  2lgs  16321  2lgsoddprm  16330  umgrnloop2  16490  uhgr2edg  16545  umgrclwwlkge2  16741