Theorem nesymi 2466

Description: Inference associated with nesym 2465. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
nesymi.1	|- A =/= B

Assertion

Ref	Expression
nesymi	|- -. B = A

Proof of Theorem nesymi

Step	Hyp	Ref	Expression
1		nesymi.1	. 2 |- A =/= B
2		nesym 2465	. 2 |- ( A =/= B <-> -. B = A )
3	1, 2	mpbi 145	1 |- -. B = A

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  16386  2lgslem4  16388  structiedg0val  16447  3dom  17184  pwle2  17194  exmidpeirce  17204  wexmiddifxylem  17211  nninfalllem1  17217  nninfall  17218  nninfsellemeq  17223  trirec0xor  17261