Theorem nesymi 2410

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

Hypothesis

Ref	Expression
nesymi.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
nesymi	⊢ ¬ 𝐵 = 𝐴

Proof of Theorem nesymi

Step	Hyp	Ref	Expression
1		nesymi.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		nesym 2409	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ ¬ 𝐵 = 𝐴

Syntax hints:  ¬ wn 3   = wceq 1364   ≠ wne 2364

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 1458  ax-gen 1460  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-ne 2365

This theorem is referenced by:  frec0g  6452  djune  7139  omp1eomlem  7155  fodjum  7207  fodju0  7208  ismkvnex  7216  mkvprop  7219  omniwomnimkv  7228  3nelsucpw1  7296  xrltnr  9848  nltmnf  9857  xnn0xadd0  9936  fnpr2ob  12926  2lgslem3  15258  2lgslem4  15260  pwle2  15559  nninfalllem1  15568  nninfall  15569  nninfsellemeq  15574  trirec0xor  15605