Theorem nesymi 2460

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

Syntax hints:  ¬ wn 3   = wceq 1398   ≠ wne 2414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  frec0g  6641  2omap  7282  djune  7382  omp1eomlem  7398  fodjum  7450  fodju0  7451  ismkvnex  7459  mkvprop  7462  omniwomnimkv  7471  pr2cv1  7505  3nelsucpw1  7557  xrltnr  10134  nltmnf  10143  xnn0xadd0  10222  ballotfilemi1  13192  fnpr2ob  13607  2lgslem3  16103  2lgslem4  16105  structiedg0val  16164  3dom  16901  pwle2  16911  exmidpeirce  16920  nninfalllem1  16925  nninfall  16926  nninfsellemeq  16931  trirec0xor  16968