Theorem necomi 2497

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 2496	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	mpbi 145	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ≠ wne 2412

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  0nep0  4277  xp01disj  6665  xp01disjl  6666  rex2dom  7062  djulclb  7345  djuinr  7353  2oneel  7569  pnfnemnf  8327  mnfnepnf  8328  ltneii  8369  1ne0  9304  0ne2  9442  fzprval  10415  0tonninf  10801  1tonninf  10802  ressplusgd  13334  ressmulrg  13350  fnpr2o  13544  fvpr0o  13546  fvpr1o  13547  mgpress  14067  rmodislmod  14491  sralemg  14578  srascag  14582  sratsetg  14585  sradsg  14588  zlmbasg  14769  zlmplusgg  14770  zlmmulrg  14771  zlmsca  14772  znbas2  14780  znadd  14781  znmul  14782  usgrexmpldifpr  16236  konigsbergiedgwen  16471  konigsberglem2  16476  konigsberglem3  16477  konigsberglem5  16479