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

Syntax hints:   =/= wne 2420

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced by:  0nep0  4297  xp01disj  6696  xp01disjl  6697  rex2dom  7100  djulclb  7385  djuinr  7393  2oneel  7612  pnfnemnf  8370  mnfnepnf  8371  ltneii  8412  1ne0  9351  0ne2  9489  fzprval  10467  0tonninf  10855  1tonninf  10856  ressplusgd  13460  ressmulrg  13476  fnpr2o  13637  fvpr0o  13639  fvpr1o  13640  mgpress  14205  rmodislmod  14660  sralemg  14747  srascag  14751  sratsetg  14754  sradsg  14757  zlmbasg  14936  zlmplusgg  14937  zlmmulrg  14938  zlmsca  14939  znbas2  14947  znadd  14948  znmul  14949  usgrexmpldifpr  16404  konigsbergiedgwen  16639  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647