Theorem necomi 2452

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

Syntax hints:   ≠ wne 2367

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 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  0nep0  4199  xp01disj  6500  xp01disjl  6501  djulclb  7130  djuinr  7138  2oneel  7341  pnfnemnf  8100  mnfnepnf  8101  ltneii  8142  1ne0  9077  0ne2  9215  fzprval  10176  0tonninf  10551  1tonninf  10552  ressplusgd  12833  ressmulrg  12849  fnpr2o  13043  fvpr0o  13045  fvpr1o  13046  mgpress  13565  rmodislmod  13985  sralemg  14072  srascag  14076  sratsetg  14079  sradsg  14082  zlmbasg  14263  zlmplusgg  14264  zlmmulrg  14265  zlmsca  14266  znbas2  14274  znadd  14275  znmul  14276