Theorem necomi 2485

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

Syntax hints:   ≠ wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  0nep0  4248  xp01disj  6569  xp01disjl  6570  rex2dom  6961  djulclb  7210  djuinr  7218  2oneel  7430  pnfnemnf  8189  mnfnepnf  8190  ltneii  8231  1ne0  9166  0ne2  9304  fzprval  10266  0tonninf  10649  1tonninf  10650  ressplusgd  13148  ressmulrg  13164  fnpr2o  13358  fvpr0o  13360  fvpr1o  13361  mgpress  13880  rmodislmod  14300  sralemg  14387  srascag  14391  sratsetg  14394  sradsg  14397  zlmbasg  14578  zlmplusgg  14579  zlmmulrg  14580  zlmsca  14581  znbas2  14589  znadd  14590  znmul  14591