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  6710  xp01disjl  6711  rex2dom  7115  djulclb  7402  djuinr  7410  2oneel  7629  pnfnemnf  8387  mnfnepnf  8388  ltneii  8430  1ne0  9382  0ne2  9522  fzprval  10507  0tonninf  10899  1tonninf  10900  ressplusgd  13543  ressmulrg  13559  fnpr2o  13720  fvpr0o  13722  fvpr1o  13723  mgpress  14338  rmodislmod  14798  sralemg  14885  srascag  14889  sratsetg  14892  sradsg  14895  zlmbasg  15074  zlmplusgg  15075  zlmmulrg  15076  zlmsca  15077  znbas2  15085  znadd  15086  znmul  15087  usgrexmpldifpr  16707  konigsbergiedgwen  16942  konigsberglem2  16947  konigsberglem3  16948  konigsberglem5  16950