Theorem necomi 2487

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

Syntax hints:   =/= wne 2402

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 619  ax-in2 620  ax-5 1495  ax-gen 1497  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2403

This theorem is referenced by:  0nep0  4255  xp01disj  6600  xp01disjl  6601  rex2dom  6995  djulclb  7253  djuinr  7261  2oneel  7474  pnfnemnf  8233  mnfnepnf  8234  ltneii  8275  1ne0  9210  0ne2  9348  fzprval  10316  0tonninf  10701  1tonninf  10702  ressplusgd  13211  ressmulrg  13227  fnpr2o  13421  fvpr0o  13423  fvpr1o  13424  mgpress  13943  rmodislmod  14364  sralemg  14451  srascag  14455  sratsetg  14458  sradsg  14461  zlmbasg  14642  zlmplusgg  14643  zlmmulrg  14644  zlmsca  14645  znbas2  14653  znadd  14654  znmul  14655  usgrexmpldifpr  16099