Theorem nesymi 2355

Description: Inference associated with nesym 2354. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
nesymi.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
nesymi	⊢ ¬ 𝐵 = 𝐴

Proof of Theorem nesymi

Step	Hyp	Ref	Expression
1		nesymi.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		nesym 2354	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
3	1, 2	mpbi 144	1 ⊢ ¬ 𝐵 = 𝐴

Syntax hints:  ¬ wn 3   = wceq 1332   ≠ wne 2309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1424  ax-gen 1426  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-ne 2310

This theorem is referenced by:  frec0g  6302  djune  6971  omp1eomlem  6987  fodjum  7026  fodju0  7027  ismkvnex  7037  mkvprop  7040  omniwomnimkv  7049  xrltnr  9596  nltmnf  9604  xnn0xadd0  9680  pwle2  13366  nninfalllem1  13378  nninfall  13379  nninfsellemeq  13385  trirec0xor  13413