Theorem necomi 2452

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

Syntax hints:   =/= wne 2367

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 615  ax-in2 616  ax-5 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  0nep0  4198  xp01disj  6491  xp01disjl  6492  djulclb  7121  djuinr  7129  2oneel  7323  pnfnemnf  8081  mnfnepnf  8082  ltneii  8123  1ne0  9058  0ne2  9196  fzprval  10157  0tonninf  10532  1tonninf  10533  ressplusgd  12806  ressmulrg  12822  fnpr2o  12982  fvpr0o  12984  fvpr1o  12985  mgpress  13487  rmodislmod  13907  sralemg  13994  srascag  13998  sratsetg  14001  sradsg  14004  zlmbasg  14185  zlmplusgg  14186  zlmmulrg  14187  zlmsca  14188  znbas2  14196  znadd  14197  znmul  14198