Theorem necomi 2485

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

Syntax hints:   =/= wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  0nep0  4253  xp01disj  6596  xp01disjl  6597  rex2dom  6991  djulclb  7245  djuinr  7253  2oneel  7465  pnfnemnf  8224  mnfnepnf  8225  ltneii  8266  1ne0  9201  0ne2  9339  fzprval  10307  0tonninf  10692  1tonninf  10693  ressplusgd  13202  ressmulrg  13218  fnpr2o  13412  fvpr0o  13414  fvpr1o  13415  mgpress  13934  rmodislmod  14355  sralemg  14442  srascag  14446  sratsetg  14449  sradsg  14452  zlmbasg  14633  zlmplusgg  14634  zlmmulrg  14635  zlmsca  14636  znbas2  14644  znadd  14645  znmul  14646  usgrexmpldifpr  16088