Theorem eqneqall 2410

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   =/= wne 2400

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

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

This theorem is referenced by:  ssprsseq  3830  eldju2ndl  7250  eldju2ndr  7251  modfzo0difsn  10629  nno  12433  prm2orodd  12664  prm23lt5  12802  dvdsprmpweqnn  12875  logbgcd1irr  15657  gausslemma2dlem0f  15749  gausslemma2dlem0i  15752  2lgs  15799  2lgsoddprm  15808  umgrnloop2  15965  uhgr2edg  16020  umgrclwwlkge2  16145