Theorem nesymi 2421

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

Syntax hints:   -. wn 3   = wceq 1372   =/= wne 2375

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 615  ax-in2 616  ax-5 1469  ax-gen 1471  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-ne 2376

This theorem is referenced by:  frec0g  6482  djune  7179  omp1eomlem  7195  fodjum  7247  fodju0  7248  ismkvnex  7256  mkvprop  7259  omniwomnimkv  7268  3nelsucpw1  7345  xrltnr  9900  nltmnf  9909  xnn0xadd0  9988  fnpr2ob  13143  2lgslem3  15549  2lgslem4  15551  structiedg0val  15608  2omap  15894  pwle2  15897  nninfalllem1  15907  nninfall  15908  nninfsellemeq  15913  trirec0xor  15946