Theorem nesymi 2460

Description: Inference associated with nesym 2459. (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 2459	. 2 |- ( A =/= B <-> -. B = A )
3	1, 2	mpbi 145	1 |- -. B = A

Syntax hints:   -. wn 3   = wceq 1398   =/= wne 2414

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  frec0g  6641  2omap  7282  djune  7382  omp1eomlem  7398  fodjum  7450  fodju0  7451  ismkvnex  7459  mkvprop  7462  omniwomnimkv  7471  pr2cv1  7505  3nelsucpw1  7557  xrltnr  10131  nltmnf  10140  xnn0xadd0  10219  ballotfilemi1  13189  fnpr2ob  13604  2lgslem3  16100  2lgslem4  16102  structiedg0val  16161  3dom  16888  pwle2  16898  exmidpeirce  16907  nninfalllem1  16912  nninfall  16913  nninfsellemeq  16918  trirec0xor  16955