Theorem eqneqall 2430

Description: A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)

Assertion

Ref	Expression
eqneqall	⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))

Proof of Theorem eqneqall

Step	Hyp	Ref	Expression
1		df-ne 2421	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		pm2.24 630	. 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐴 = 𝐵 → 𝜑))
3	1, 2	biimtrid 152	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))

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  10852  nno  12697  prm2orodd  12928  prm23lt5  13070  dvdsprmpweqnn  13143  logbgcd1irr  16220  gausslemma2dlem0f  16395  gausslemma2dlem0i  16398  2lgs  16445  2lgsoddprm  16454  umgrnloop2  16614  uhgr2edg  16669  umgrclwwlkge2  16865