Theorem necomd 2489

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

Hypothesis

Ref	Expression
necomd.1	|- ( ph -> A =/= B )

Assertion

Ref	Expression
necomd	|- ( ph -> B =/= A )

Proof of Theorem necomd

Step	Hyp	Ref	Expression
1		necomd.1	. 2 |- ( ph -> A =/= B )
2		necom 2487	. 2 |- ( A =/= B <-> B =/= A )
3	1, 2	sylib 122	1 |- ( ph -> B =/= A )

Syntax hints:   -> wi 4   =/= wne 2403

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 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2404

This theorem is referenced by:  ifnefals  3654  difsnb  3821  0nelop  4346  frecabcl  6608  fidifsnen  7100  tpfidisj  7164  omp1eomlem  7336  difinfsnlem  7341  fodjuomnilemdc  7386  en2eleq  7449  en2other2  7450  netap  7516  2omotaplemap  7519  ltned  8335  lt0ne0  8650  zdceq  9599  zneo  9625  xrlttri3  10076  qdceq  10550  flqltnz  10593  seqf1oglem1  10827  nn0opthd  11030  hashdifpr  11130  hashtpgim  11155  cats1un  11351  sumtp  12038  nninfctlemfo  12674  isprm2lem  12751  oddprm  12895  pcmpt  12979  ennnfonelemex  13098  perfectlem2  15797  lgsneg  15826  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem3  15881  lgsquad2  15885  2lgsoddprm  15915  funvtxval0d  15957  umgrvad2edg  16135  1hegrvtxdg1rfi  16234  vdegp1bid  16239  umgr2cwwk2dif  16348  eupth2lem3lem4fi  16397  pw1ndom3lem  16692  pw1ndom3  16693