Theorem eqneqall 2410

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 2401	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		pm2.24 624	. 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐴 = 𝐵 → 𝜑))
3	1, 2	biimtrid 152	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))

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  3833  eldju2ndl  7262  eldju2ndr  7263  modfzo0difsn  10647  nno  12457  prm2orodd  12688  prm23lt5  12826  dvdsprmpweqnn  12899  logbgcd1irr  15681  gausslemma2dlem0f  15773  gausslemma2dlem0i  15776  2lgs  15823  2lgsoddprm  15832  umgrnloop2  15990  uhgr2edg  16045  umgrclwwlkge2  16197