Theorem necomi 2444

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

Syntax hints:   ≠ wne 2359

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 1457  ax-gen 1459  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-cleq 2181  df-ne 2360

This theorem is referenced by:  0nep0  4179  xp01disj  6451  xp01disjl  6452  djulclb  7071  djuinr  7079  2oneel  7272  pnfnemnf  8029  mnfnepnf  8030  ltneii  8071  1ne0  9004  0ne2  9141  fzprval  10099  0tonninf  10456  1tonninf  10457  ressplusgd  12605  ressmulrg  12621  fnpr2o  12780  fvpr0o  12782  fvpr1o  12783  mgpress  13245  rmodislmod  13627  sralemg  13714  srascag  13718  sratsetg  13721  sradsg  13724  zlmbasg  13874  zlmplusgg  13875  zlmmulrg  13876  zlmsca  13877