Theorem necomi 2499

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

Syntax hints:   ≠ wne 2414

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  0nep0  4283  xp01disj  6679  xp01disjl  6680  rex2dom  7076  djulclb  7359  djuinr  7367  2oneel  7586  pnfnemnf  8344  mnfnepnf  8345  ltneii  8386  1ne0  9325  0ne2  9463  fzprval  10441  0tonninf  10829  1tonninf  10830  ressplusgd  13430  ressmulrg  13446  fnpr2o  13607  fvpr0o  13609  fvpr1o  13610  mgpress  14174  rmodislmod  14629  sralemg  14716  srascag  14720  sratsetg  14723  sradsg  14726  zlmbasg  14907  zlmplusgg  14908  zlmmulrg  14909  zlmsca  14910  znbas2  14918  znadd  14919  znmul  14920  usgrexmpldifpr  16374  konigsbergiedgwen  16609  konigsberglem2  16614  konigsberglem3  16615  konigsberglem5  16617