Theorem necomd 2486

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 2484	. 2 |- ( A =/= B <-> B =/= A )
3	1, 2	sylib 122	1 |- ( ph -> B =/= A )

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

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  ifnefals  3648  difsnb  3814  0nelop  4338  frecabcl  6560  fidifsnen  7052  tpfidisj  7114  omp1eomlem  7284  difinfsnlem  7289  fodjuomnilemdc  7334  en2eleq  7396  en2other2  7397  netap  7463  2omotaplemap  7466  ltned  8283  lt0ne0  8598  zdceq  9545  zneo  9571  xrlttri3  10022  qdceq  10494  flqltnz  10537  seqf1oglem1  10771  nn0opthd  10974  hashdifpr  11074  cats1un  11292  sumtp  11965  nninfctlemfo  12601  isprm2lem  12678  oddprm  12822  pcmpt  12906  ennnfonelemex  13025  perfectlem2  15714  lgsneg  15743  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem3  15798  lgsquad2  15802  2lgsoddprm  15832  funvtxval0d  15874  umgrvad2edg  16050  umgr2cwwk2dif  16219  pw1ndom3lem  16524  pw1ndom3  16525