Theorem necomi 2499

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

Syntax hints:   =/= wne 2414

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 1496  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  0nep0  4283  xp01disj  6679  xp01disjl  6680  rex2dom  7076  djulclb  7359  djuinr  7367  2oneel  7586  pnfnemnf  8344  mnfnepnf  8345  ltneii  8386  1ne0  9322  0ne2  9460  fzprval  10438  0tonninf  10826  1tonninf  10827  ressplusgd  13426  ressmulrg  13442  fnpr2o  13603  fvpr0o  13605  fvpr1o  13606  mgpress  14170  rmodislmod  14625  sralemg  14712  srascag  14716  sratsetg  14719  sradsg  14722  zlmbasg  14903  zlmplusgg  14904  zlmmulrg  14905  zlmsca  14906  znbas2  14914  znadd  14915  znmul  14916  usgrexmpldifpr  16370  konigsbergiedgwen  16605  konigsberglem2  16610  konigsberglem3  16611  konigsberglem5  16613