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  10832  nno  12673  prm2orodd  12904  prm23lt5  13042  dvdsprmpweqnn  13115  logbgcd1irr  16069  gausslemma2dlem0f  16173  gausslemma2dlem0i  16176  2lgs  16223  2lgsoddprm  16232  umgrnloop2  16392  uhgr2edg  16447  umgrclwwlkge2  16643