Theorem nesymi 2386

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

Syntax hints:  ¬ wn 3   = wceq 1348   ≠ wne 2340

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 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341

This theorem is referenced by:  frec0g  6376  djune  7055  omp1eomlem  7071  fodjum  7122  fodju0  7123  ismkvnex  7131  mkvprop  7134  omniwomnimkv  7143  3nelsucpw1  7211  xrltnr  9736  nltmnf  9745  xnn0xadd0  9824  pwle2  14031  nninfalllem1  14041  nninfall  14042  nninfsellemeq  14047  trirec0xor  14077