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  6668  2omap  7318  djune  7418  omp1eomlem  7434  fodjum  7486  fodju0  7487  ismkvnex  7495  mkvprop  7498  omniwomnimkv  7507  pr2cv1  7541  3nelsucpw1  7593  xrltnr  10191  nltmnf  10200  xnn0xadd0  10279  ballotfilemi1  13294  fnpr2ob  13710  2lgslem3  16339  2lgslem4  16341  structiedg0val  16400  3dom  17137  pwle2  17147  exmidpeirce  17157  wexmiddifxylem  17164  nninfalllem1  17170  nninfall  17171  nninfsellemeq  17176  trirec0xor  17213