Theorem necomi 2460

Description: Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)

Hypothesis

Ref	Expression
necomi.1	|- A =/= B

Assertion

Ref	Expression
necomi	|- B =/= A

Proof of Theorem necomi

Step	Hyp	Ref	Expression
1		necomi.1	. 2 |- A =/= B
2		necom 2459	. 2 |- ( A =/= B <-> B =/= A )
3	1, 2	mpbi 145	1 |- B =/= A

Syntax hints:   =/= 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:  0nep0  4208  xp01disj  6518  xp01disjl  6519  rex2dom  6909  djulclb  7156  djuinr  7164  2oneel  7367  pnfnemnf  8126  mnfnepnf  8127  ltneii  8168  1ne0  9103  0ne2  9241  fzprval  10203  0tonninf  10583  1tonninf  10584  ressplusgd  12932  ressmulrg  12948  fnpr2o  13142  fvpr0o  13144  fvpr1o  13145  mgpress  13664  rmodislmod  14084  sralemg  14171  srascag  14175  sratsetg  14178  sradsg  14181  zlmbasg  14362  zlmplusgg  14363  zlmmulrg  14364  zlmsca  14365  znbas2  14373  znadd  14374  znmul  14375