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

Syntax hints:   -. wn 3   = wceq 1402   =/= wne 2420

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  frec0g  6658  2omap  7308  djune  7408  omp1eomlem  7424  fodjum  7476  fodju0  7477  ismkvnex  7485  mkvprop  7488  omniwomnimkv  7497  pr2cv1  7531  3nelsucpw1  7583  xrltnr  10160  nltmnf  10169  xnn0xadd0  10248  ballotfilemi1  13223  fnpr2ob  13638  2lgslem3  16134  2lgslem4  16136  structiedg0val  16195  3dom  16932  pwle2  16942  exmidpeirce  16951  nninfalllem1  16956  nninfall  16957  nninfsellemeq  16962  trirec0xor  16999