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  4304  xp01disj  6711  xp01disjl  6712  rex2dom  7116  djulclb  7402  djuinr  7410  2oneel  7629  pnfnemnf  8387  mnfnepnf  8388  ltneii  8430  1ne0  9382  0ne2  9522  fzprval  10506  0tonninf  10898  1tonninf  10899  ressplusgd  13542  ressmulrg  13558  fnpr2o  13719  fvpr0o  13721  fvpr1o  13722  mgpress  14337  rmodislmod  14797  sralemg  14884  srascag  14888  sratsetg  14891  sradsg  14894  zlmbasg  15073  zlmplusgg  15074  zlmmulrg  15075  zlmsca  15076  znbas2  15084  znadd  15085  znmul  15086  usgrexmpldifpr  16728  konigsbergiedgwen  16963  konigsberglem2  16968  konigsberglem3  16969  konigsberglem5  16971