Theorem nesymi 2405

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

Syntax hints:   -. wn 3   = wceq 1363   =/= wne 2359

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 1457  ax-gen 1459  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-cleq 2181  df-ne 2360

This theorem is referenced by:  frec0g  6415  djune  7094  omp1eomlem  7110  fodjum  7161  fodju0  7162  ismkvnex  7170  mkvprop  7173  omniwomnimkv  7182  3nelsucpw1  7250  xrltnr  9796  nltmnf  9805  xnn0xadd0  9884  fnpr2ob  12781  pwle2  15132  nninfalllem1  15141  nninfall  15142  nninfsellemeq  15147  trirec0xor  15177