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  4248  xp01disj  6577  xp01disjl  6578  rex2dom  6969  djulclb  7218  djuinr  7226  2oneel  7438  pnfnemnf  8197  mnfnepnf  8198  ltneii  8239  1ne0  9174  0ne2  9312  fzprval  10274  0tonninf  10657  1tonninf  10658  ressplusgd  13157  ressmulrg  13173  fnpr2o  13367  fvpr0o  13369  fvpr1o  13370  mgpress  13889  rmodislmod  14309  sralemg  14396  srascag  14400  sratsetg  14403  sradsg  14406  zlmbasg  14587  zlmplusgg  14588  zlmmulrg  14589  zlmsca  14590  znbas2  14598  znadd  14599  znmul  14600