Theorem necomi 2485

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

Syntax hints:   ≠ wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  0nep0  4250  xp01disj  6592  xp01disjl  6593  rex2dom  6984  djulclb  7238  djuinr  7246  2oneel  7458  pnfnemnf  8217  mnfnepnf  8218  ltneii  8259  1ne0  9194  0ne2  9332  fzprval  10295  0tonninf  10679  1tonninf  10680  ressplusgd  13183  ressmulrg  13199  fnpr2o  13393  fvpr0o  13395  fvpr1o  13396  mgpress  13915  rmodislmod  14336  sralemg  14423  srascag  14427  sratsetg  14430  sradsg  14433  zlmbasg  14614  zlmplusgg  14615  zlmmulrg  14616  zlmsca  14617  znbas2  14625  znadd  14626  znmul  14627  usgrexmpldifpr  16068