Theorem necomd 2488

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

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

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 1495  ax-gen 1497  ax-ext 2213

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

This theorem is referenced by:  ifnefals  3650  difsnb  3816  0nelop  4340  frecabcl  6564  fidifsnen  7056  tpfidisj  7120  omp1eomlem  7292  difinfsnlem  7297  fodjuomnilemdc  7342  en2eleq  7405  en2other2  7406  netap  7472  2omotaplemap  7475  ltned  8292  lt0ne0  8607  zdceq  9554  zneo  9580  xrlttri3  10031  qdceq  10503  flqltnz  10546  seqf1oglem1  10780  nn0opthd  10983  hashdifpr  11083  cats1un  11301  sumtp  11974  nninfctlemfo  12610  isprm2lem  12687  oddprm  12831  pcmpt  12915  ennnfonelemex  13034  perfectlem2  15723  lgsneg  15752  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem3  15807  lgsquad2  15811  2lgsoddprm  15841  funvtxval0d  15883  umgrvad2edg  16061  1hegrvtxdg1rfi  16160  vdegp1bid  16165  umgr2cwwk2dif  16274  pw1ndom3lem  16588  pw1ndom3  16589