Theorem necomi 2449

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

Syntax hints:   =/= wne 2364

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 1458  ax-gen 1460  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-ne 2365

This theorem is referenced by:  0nep0  4194  xp01disj  6486  xp01disjl  6487  djulclb  7114  djuinr  7122  2oneel  7316  pnfnemnf  8074  mnfnepnf  8075  ltneii  8116  1ne0  9050  0ne2  9187  fzprval  10148  0tonninf  10511  1tonninf  10512  ressplusgd  12746  ressmulrg  12762  fnpr2o  12922  fvpr0o  12924  fvpr1o  12925  mgpress  13427  rmodislmod  13847  sralemg  13934  srascag  13938  sratsetg  13941  sradsg  13944  zlmbasg  14117  zlmplusgg  14118  zlmmulrg  14119  zlmsca  14120  znbas2  14128  znadd  14129  znmul  14130