Theorem nesymi 2382

Description: Inference associated with nesym 2381. (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 2381	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
3	1, 2	mpbi 144	1 ⊢ ¬ 𝐵 = 𝐴

Syntax hints:  ¬ wn 3   = wceq 1343   ≠ wne 2336

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 1435  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-ne 2337

This theorem is referenced by:  frec0g  6365  djune  7043  omp1eomlem  7059  fodjum  7110  fodju0  7111  ismkvnex  7119  mkvprop  7122  omniwomnimkv  7131  3nelsucpw1  7190  xrltnr  9715  nltmnf  9724  xnn0xadd0  9803  pwle2  13888  nninfalllem1  13898  nninfall  13899  nninfsellemeq  13904  trirec0xor  13934