Theorem necomi 2505

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

This proof depends on syntax axioms:   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  0nep0  4302  xp01disj  6706  xp01disjl  6707  rex2dom  7110  djulclb  7395  djuinr  7403  2oneel  7622  pnfnemnf  8380  mnfnepnf  8381  ltneii  8422  1ne0  9373  0ne2  9512  fzprval  10491  0tonninf  10879  1tonninf  10880  ressplusgd  13485  ressmulrg  13501  fnpr2o  13662  fvpr0o  13664  fvpr1o  13665  mgpress  14232  rmodislmod  14690  sralemg  14777  srascag  14781  sratsetg  14784  sradsg  14787  zlmbasg  14966  zlmplusgg  14967  zlmmulrg  14968  zlmsca  14969  znbas2  14977  znadd  14978  znmul  14979  usgrexmpldifpr  16502  konigsbergiedgwen  16737  konigsberglem2  16742  konigsberglem3  16743  konigsberglem5  16745