Theorem necomd 2500

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 2498	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ≠ wne 2414

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  ifnefals  3669  difsnb  3839  0nelop  4366  frecabcl  6632  fidifsnen  7127  tpfidisj  7191  omp1eomlem  7387  difinfsnlem  7392  fodjuomnilemdc  7437  en2eleq  7500  en2other2  7501  netap  7573  2omotaplemap  7576  ltned  8392  lt0ne0  8707  zdceq  9658  zneo  9685  xrlttri3  10136  qdceq  10611  flqltnz  10654  seqf1oglem1  10888  nn0opthd  11092  hashdifpr  11193  hashtpgim  11225  cats1un  11421  sumtp  12108  nninfctlemfo  12744  isprm2lem  12821  oddprm  12965  pcmpt  13049  ennnfonelemex  13186  perfectlem2  15917  lgsneg  15946  lgseisenlem4  15995  lgsquadlem1  15999  lgsquadlem3  16001  lgsquad2  16005  2lgsoddprm  16035  funvtxval0d  16077  umgrvad2edg  16255  1hegrvtxdg1rfi  16354  vdegp1bid  16359  umgr2cwwk2dif  16468  eupth2lem3lem4fi  16517  pw1ndom3lem  16812  pw1ndom3  16813