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  4249  xp01disj  6587  xp01disjl  6588  rex2dom  6979  djulclb  7233  djuinr  7241  2oneel  7453  pnfnemnf  8212  mnfnepnf  8213  ltneii  8254  1ne0  9189  0ne2  9327  fzprval  10290  0tonninf  10674  1tonninf  10675  ressplusgd  13177  ressmulrg  13193  fnpr2o  13387  fvpr0o  13389  fvpr1o  13390  mgpress  13909  rmodislmod  14330  sralemg  14417  srascag  14421  sratsetg  14424  sradsg  14427  zlmbasg  14608  zlmplusgg  14609  zlmmulrg  14610  zlmsca  14611  znbas2  14619  znadd  14620  znmul  14621