Theorem necomi 2505

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

This proof depends on syntax axioms:   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  0nep0  4304  xp01disj  6711  xp01disjl  6712  rex2dom  7116  djulclb  7401  djuinr  7409  2oneel  7628  pnfnemnf  8386  mnfnepnf  8387  ltneii  8429  1ne0  9381  0ne2  9521  fzprval  10505  0tonninf  10897  1tonninf  10898  ressplusgd  13541  ressmulrg  13557  fnpr2o  13718  fvpr0o  13720  fvpr1o  13721  mgpress  14336  rmodislmod  14796  sralemg  14883  srascag  14887  sratsetg  14890  sradsg  14893  zlmbasg  15072  zlmplusgg  15073  zlmmulrg  15074  zlmsca  15075  znbas2  15083  znadd  15084  znmul  15085  usgrexmpldifpr  16712  konigsbergiedgwen  16947  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955