Theorem necomi 2488

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

Syntax hints:   =/= wne 2403

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 2213

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

This theorem is referenced by:  0nep0  4261  xp01disj  6644  xp01disjl  6645  rex2dom  7039  djulclb  7297  djuinr  7305  2oneel  7518  pnfnemnf  8276  mnfnepnf  8277  ltneii  8318  1ne0  9253  0ne2  9391  fzprval  10362  0tonninf  10748  1tonninf  10749  ressplusgd  13275  ressmulrg  13291  fnpr2o  13485  fvpr0o  13487  fvpr1o  13488  mgpress  14008  rmodislmod  14430  sralemg  14517  srascag  14521  sratsetg  14524  sradsg  14527  zlmbasg  14708  zlmplusgg  14709  zlmmulrg  14710  zlmsca  14711  znbas2  14719  znadd  14720  znmul  14721  usgrexmpldifpr  16173  konigsbergiedgwen  16408  konigsberglem2  16413  konigsberglem3  16414  konigsberglem5  16416