Theorem necomi 2497

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

Syntax hints:   =/= wne 2412

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  0nep0  4278  xp01disj  6666  xp01disjl  6667  rex2dom  7063  djulclb  7346  djuinr  7354  2oneel  7570  pnfnemnf  8328  mnfnepnf  8329  ltneii  8370  1ne0  9305  0ne2  9443  fzprval  10416  0tonninf  10802  1tonninf  10803  ressplusgd  13342  ressmulrg  13358  fnpr2o  13552  fvpr0o  13554  fvpr1o  13555  mgpress  14075  rmodislmod  14499  sralemg  14586  srascag  14590  sratsetg  14593  sradsg  14596  zlmbasg  14777  zlmplusgg  14778  zlmmulrg  14779  zlmsca  14780  znbas2  14788  znadd  14789  znmul  14790  usgrexmpldifpr  16244  konigsbergiedgwen  16479  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487