Theorem necomi 2462

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

Syntax hints:   ≠ wne 2377

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 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-ne 2378

This theorem is referenced by:  0nep0  4213  xp01disj  6526  xp01disjl  6527  rex2dom  6917  djulclb  7164  djuinr  7172  2oneel  7375  pnfnemnf  8134  mnfnepnf  8135  ltneii  8176  1ne0  9111  0ne2  9249  fzprval  10211  0tonninf  10592  1tonninf  10593  ressplusgd  13005  ressmulrg  13021  fnpr2o  13215  fvpr0o  13217  fvpr1o  13218  mgpress  13737  rmodislmod  14157  sralemg  14244  srascag  14248  sratsetg  14251  sradsg  14254  zlmbasg  14435  zlmplusgg  14436  zlmmulrg  14437  zlmsca  14438  znbas2  14446  znadd  14447  znmul  14448