Theorem necomi 2449

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

Syntax hints:   ≠ wne 2364

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 1458  ax-gen 1460  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-ne 2365

This theorem is referenced by:  0nep0  4195  xp01disj  6488  xp01disjl  6489  djulclb  7116  djuinr  7124  2oneel  7318  pnfnemnf  8076  mnfnepnf  8077  ltneii  8118  1ne0  9052  0ne2  9190  fzprval  10151  0tonninf  10514  1tonninf  10515  ressplusgd  12749  ressmulrg  12765  fnpr2o  12925  fvpr0o  12927  fvpr1o  12928  mgpress  13430  rmodislmod  13850  sralemg  13937  srascag  13941  sratsetg  13944  sradsg  13947  zlmbasg  14128  zlmplusgg  14129  zlmmulrg  14130  zlmsca  14131  znbas2  14139  znadd  14140  znmul  14141