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  7319  djune  7419  omp1eomlem  7435  fodjum  7487  fodju0  7488  ismkvnex  7496  mkvprop  7499  omniwomnimkv  7508  pr2cv1  7542  3nelsucpw1  7594  xrltnr  10192  nltmnf  10201  xnn0xadd0  10280  ballotfilemi1  13297  fnpr2ob  13714  2lgslem3  16391  2lgslem4  16393  structiedg0val  16452  3dom  17189  pwle2  17199  exmidpeirce  17209  wexmiddifxylem  17216  nninfalllem1  17222  nninfall  17223  nninfsellemeq  17228  trirec0xor  17266