Theorem necomi 2463

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 2462	. 2 |- ( A =/= B <-> B =/= A )
3	1, 2	mpbi 145	1 |- B =/= A

Syntax hints:   =/= wne 2378

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 1471  ax-gen 1473  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-ne 2379

This theorem is referenced by:  0nep0  4225  xp01disj  6542  xp01disjl  6543  rex2dom  6934  djulclb  7183  djuinr  7191  2oneel  7403  pnfnemnf  8162  mnfnepnf  8163  ltneii  8204  1ne0  9139  0ne2  9277  fzprval  10239  0tonninf  10622  1tonninf  10623  ressplusgd  13076  ressmulrg  13092  fnpr2o  13286  fvpr0o  13288  fvpr1o  13289  mgpress  13808  rmodislmod  14228  sralemg  14315  srascag  14319  sratsetg  14322  sradsg  14325  zlmbasg  14506  zlmplusgg  14507  zlmmulrg  14508  zlmsca  14509  znbas2  14517  znadd  14518  znmul  14519