Theorem necomd 2463

Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)

Hypothesis

Ref	Expression
necomd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Assertion

Ref	Expression
necomd	⊢ (𝜑 → 𝐵 ≠ 𝐴)

Proof of Theorem necomd

Step	Hyp	Ref	Expression
1		necomd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		necom 2461	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ≠ wne 2377

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 1471  ax-gen 1473  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-ne 2378

This theorem is referenced by:  ifnefals  3615  difsnb  3778  0nelop  4296  frecabcl  6492  fidifsnen  6974  tpfidisj  7033  omp1eomlem  7203  difinfsnlem  7208  fodjuomnilemdc  7253  en2eleq  7310  en2other2  7311  netap  7373  2omotaplemap  7376  ltned  8193  lt0ne0  8508  zdceq  9455  zneo  9481  xrlttri3  9926  qdceq  10394  flqltnz  10437  seqf1oglem1  10671  nn0opthd  10874  hashdifpr  10972  sumtp  11769  nninfctlemfo  12405  isprm2lem  12482  oddprm  12626  pcmpt  12710  ennnfonelemex  12829  perfectlem2  15516  lgsneg  15545  lgseisenlem4  15594  lgsquadlem1  15598  lgsquadlem3  15600  lgsquad2  15604  2lgsoddprm  15634  funvtxval0d  15676