Theorem necomi 2485

Description: Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)

Hypothesis

Ref	Expression
necomi.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
necomi	⊢ 𝐵 ≠ 𝐴

Proof of Theorem necomi

Step	Hyp	Ref	Expression
1		necomi.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		necom 2484	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	mpbi 145	1 ⊢ 𝐵 ≠ 𝐴

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  4253  xp01disj  6596  xp01disjl  6597  rex2dom  6991  djulclb  7248  djuinr  7256  2oneel  7468  pnfnemnf  8227  mnfnepnf  8228  ltneii  8269  1ne0  9204  0ne2  9342  fzprval  10310  0tonninf  10695  1tonninf  10696  ressplusgd  13205  ressmulrg  13221  fnpr2o  13415  fvpr0o  13417  fvpr1o  13418  mgpress  13937  rmodislmod  14358  sralemg  14445  srascag  14449  sratsetg  14452  sradsg  14455  zlmbasg  14636  zlmplusgg  14637  zlmmulrg  14638  zlmsca  14639  znbas2  14647  znadd  14648  znmul  14649  usgrexmpldifpr  16093