Theorem necomi 2432

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

Syntax hints:   =/= wne 2347

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  0nep0  4167  xp01disj  6436  xp01disjl  6437  djulclb  7056  djuinr  7064  2oneel  7257  pnfnemnf  8014  mnfnepnf  8015  ltneii  8056  1ne0  8989  0ne2  9126  fzprval  10084  0tonninf  10441  1tonninf  10442  ressplusgd  12589  ressmulrg  12605  fnpr2o  12763  fvpr0o  12765  fvpr1o  12766  mgpress  13146  rmodislmod  13446