Theorem necomi 2488

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

Syntax hints:   ≠ wne 2403

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 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2404

This theorem is referenced by:  0nep0  4261  xp01disj  6644  xp01disjl  6645  rex2dom  7039  djulclb  7297  djuinr  7305  2oneel  7518  pnfnemnf  8277  mnfnepnf  8278  ltneii  8319  1ne0  9254  0ne2  9392  fzprval  10360  0tonninf  10746  1tonninf  10747  ressplusgd  13273  ressmulrg  13289  fnpr2o  13483  fvpr0o  13485  fvpr1o  13486  mgpress  14006  rmodislmod  14427  sralemg  14514  srascag  14518  sratsetg  14521  sradsg  14524  zlmbasg  14705  zlmplusgg  14706  zlmmulrg  14707  zlmsca  14708  znbas2  14716  znadd  14717  znmul  14718  usgrexmpldifpr  16170  konigsbergiedgwen  16405  konigsberglem2  16410  konigsberglem3  16411  konigsberglem5  16413