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  4302  xp01disj  6706  xp01disjl  6707  rex2dom  7110  djulclb  7396  djuinr  7404  2oneel  7623  pnfnemnf  8381  mnfnepnf  8382  ltneii  8424  1ne0  9375  0ne2  9515  fzprval  10500  0tonninf  10891  1tonninf  10892  ressplusgd  13534  ressmulrg  13550  fnpr2o  13711  fvpr0o  13713  fvpr1o  13714  mgpress  14281  rmodislmod  14739  sralemg  14826  srascag  14830  sratsetg  14833  sradsg  14836  zlmbasg  15015  zlmplusgg  15016  zlmmulrg  15017  zlmsca  15018  znbas2  15026  znadd  15027  znmul  15028  usgrexmpldifpr  16612  konigsbergiedgwen  16847  konigsberglem2  16852  konigsberglem3  16853  konigsberglem5  16855