Theorem necomd 2506

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

This proof depends on syntax axioms:   → wi 4   ≠ 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:  ifnefals  3685  difsnb  3858  0nelop  4388  frecabcl  6670  fidifsnen  7172  tpfidisj  7236  omp1eomlem  7434  difinfsnlem  7439  fodjuomnilemdc  7484  en2eleq  7547  en2other2  7548  netap  7620  2omotaplemap  7623  ltned  8439  lt0ne0  8756  zdceq  9722  zneo  9749  xrlttri3  10201  qdceq  10681  flqltnz  10724  seqf1oglem1  10958  nn0opthd  11162  hashdifpr  11263  hashtpgim  11299  cats1un  11495  sumtp  12183  nninfctlemfo  12819  isprm2lem  12896  oddprm  13040  pcmpt  13124  ennnfonelemex  13307  perfectlem2  16120  lgsneg  16155  lgseisenlem4  16204  lgsquadlem1  16208  lgsquadlem3  16210  lgsquad2  16214  2lgsoddprm  16244  funvtxval0d  16286  umgrvad2edg  16464  1hegrvtxdg1rfi  16563  vdegp1bid  16568  umgr2cwwk2dif  16677  eupth2lem3lem4fi  16726  pw1ndom3lem  17031  pw1ndom3  17032