Theorem necomi 2505

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

Syntax hints:   ≠ wne 2420

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  0nep0  4300  xp01disj  6700  xp01disjl  6701  rex2dom  7104  djulclb  7389  djuinr  7397  2oneel  7616  pnfnemnf  8374  mnfnepnf  8375  ltneii  8416  1ne0  9355  0ne2  9493  fzprval  10472  0tonninf  10860  1tonninf  10861  ressplusgd  13466  ressmulrg  13482  fnpr2o  13643  fvpr0o  13645  fvpr1o  13646  mgpress  14213  rmodislmod  14671  sralemg  14758  srascag  14762  sratsetg  14765  sradsg  14768  zlmbasg  14947  zlmplusgg  14948  zlmmulrg  14949  zlmsca  14950  znbas2  14958  znadd  14959  znmul  14960  usgrexmpldifpr  16473  konigsbergiedgwen  16708  konigsberglem2  16713  konigsberglem3  16714  konigsberglem5  16716