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  3647  difsnb  3811  0nelop  4334  frecabcl  6551  fidifsnen  7040  tpfidisj  7102  omp1eomlem  7272  difinfsnlem  7277  fodjuomnilemdc  7322  en2eleq  7384  en2other2  7385  netap  7451  2omotaplemap  7454  ltned  8271  lt0ne0  8586  zdceq  9533  zneo  9559  xrlttri3  10005  qdceq  10476  flqltnz  10519  seqf1oglem1  10753  nn0opthd  10956  hashdifpr  11055  cats1un  11268  sumtp  11940  nninfctlemfo  12576  isprm2lem  12653  oddprm  12797  pcmpt  12881  ennnfonelemex  13000  perfectlem2  15689  lgsneg  15718  lgseisenlem4  15767  lgsquadlem1  15771  lgsquadlem3  15773  lgsquad2  15777  2lgsoddprm  15807  funvtxval0d  15849  umgrvad2edg  16024  pw1ndom3lem  16412  pw1ndom3  16413