Theorem nesymi 2426

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

Syntax hints:  ¬ wn 3   = wceq 1375   ≠ wne 2380

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 617  ax-in2 618  ax-5 1473  ax-gen 1475  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-ne 2381

This theorem is referenced by:  frec0g  6513  djune  7213  omp1eomlem  7229  fodjum  7281  fodju0  7282  ismkvnex  7290  mkvprop  7293  omniwomnimkv  7302  pr2cv1  7336  3nelsucpw1  7387  xrltnr  9943  nltmnf  9952  xnn0xadd0  10031  fnpr2ob  13339  2lgslem3  15745  2lgslem4  15747  structiedg0val  15806  2omap  16270  pwle2  16275  nninfalllem1  16285  nninfall  16286  nninfsellemeq  16291  trirec0xor  16324