Theorem necomi 2487

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

Syntax hints:   ≠ wne 2402

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 1495  ax-gen 1497  ax-ext 2213

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

This theorem is referenced by:  0nep0  4255  xp01disj  6601  xp01disjl  6602  rex2dom  6996  djulclb  7254  djuinr  7262  2oneel  7475  pnfnemnf  8234  mnfnepnf  8235  ltneii  8276  1ne0  9211  0ne2  9349  fzprval  10317  0tonninf  10703  1tonninf  10704  ressplusgd  13217  ressmulrg  13233  fnpr2o  13427  fvpr0o  13429  fvpr1o  13430  mgpress  13950  rmodislmod  14371  sralemg  14458  srascag  14462  sratsetg  14465  sradsg  14468  zlmbasg  14649  zlmplusgg  14650  zlmmulrg  14651  zlmsca  14652  znbas2  14660  znadd  14661  znmul  14662  usgrexmpldifpr  16106