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  4249  xp01disj  6587  xp01disjl  6588  rex2dom  6979  djulclb  7230  djuinr  7238  2oneel  7450  pnfnemnf  8209  mnfnepnf  8210  ltneii  8251  1ne0  9186  0ne2  9324  fzprval  10286  0tonninf  10670  1tonninf  10671  ressplusgd  13170  ressmulrg  13186  fnpr2o  13380  fvpr0o  13382  fvpr1o  13383  mgpress  13902  rmodislmod  14323  sralemg  14410  srascag  14414  sratsetg  14417  sradsg  14420  zlmbasg  14601  zlmplusgg  14602  zlmmulrg  14603  zlmsca  14604  znbas2  14612  znadd  14613  znmul  14614