Theorem necomi 2452

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

Syntax hints:   =/= wne 2367

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 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  0nep0  4199  xp01disj  6500  xp01disjl  6501  djulclb  7130  djuinr  7138  2oneel  7339  pnfnemnf  8098  mnfnepnf  8099  ltneii  8140  1ne0  9075  0ne2  9213  fzprval  10174  0tonninf  10549  1tonninf  10550  ressplusgd  12831  ressmulrg  12847  fnpr2o  13041  fvpr0o  13043  fvpr1o  13044  mgpress  13563  rmodislmod  13983  sralemg  14070  srascag  14074  sratsetg  14077  sradsg  14080  zlmbasg  14261  zlmplusgg  14262  zlmmulrg  14263  zlmsca  14264  znbas2  14272  znadd  14273  znmul  14274