Theorem necomi 2461

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

Syntax hints:   =/= wne 2376

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 1470  ax-gen 1472  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-ne 2377

This theorem is referenced by:  0nep0  4209  xp01disj  6519  xp01disjl  6520  rex2dom  6910  djulclb  7157  djuinr  7165  2oneel  7368  pnfnemnf  8127  mnfnepnf  8128  ltneii  8169  1ne0  9104  0ne2  9242  fzprval  10204  0tonninf  10585  1tonninf  10586  ressplusgd  12961  ressmulrg  12977  fnpr2o  13171  fvpr0o  13173  fvpr1o  13174  mgpress  13693  rmodislmod  14113  sralemg  14200  srascag  14204  sratsetg  14207  sradsg  14210  zlmbasg  14391  zlmplusgg  14392  zlmmulrg  14393  zlmsca  14394  znbas2  14402  znadd  14403  znmul  14404