Theorem nesymi 2466

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  frec0g  6672  2omap  7325  djune  7425  omp1eomlem  7441  fodjum  7493  fodju0  7494  ismkvnex  7502  mkvprop  7505  omniwomnimkv  7514  pr2cv1  7548  3nelsucpw1  7600  xrltnr  10199  nltmnf  10208  xnn0xadd0  10287  ballotfilemi1  13304  fnpr2ob  13721  2lgslem3  16437  2lgslem4  16439  structiedg0val  16498  3dom  17235  pwle2  17245  exmidpeirce  17255  wexmiddifxylem  17262  nninfalllem1  17269  nninfall  17270  nninfsellemeq  17275  trirec0xor  17313