Theorem nesymi 2373

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

Syntax hints:  ¬ wn 3   = wceq 1335   ≠ wne 2327

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 1427  ax-gen 1429  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-ne 2328

This theorem is referenced by:  frec0g  6344  djune  7022  omp1eomlem  7038  fodjum  7089  fodju0  7090  ismkvnex  7098  mkvprop  7101  omniwomnimkv  7110  3nelsucpw1  7169  xrltnr  9686  nltmnf  9695  xnn0xadd0  9771  pwle2  13581  nninfalllem1  13591  nninfall  13592  nninfsellemeq  13597  trirec0xor  13627