Theorem necomd 2463

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

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

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 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-ne 2378

This theorem is referenced by:  ifnefals  3619  difsnb  3782  0nelop  4300  frecabcl  6498  fidifsnen  6982  tpfidisj  7041  omp1eomlem  7211  difinfsnlem  7216  fodjuomnilemdc  7261  en2eleq  7319  en2other2  7320  netap  7386  2omotaplemap  7389  ltned  8206  lt0ne0  8521  zdceq  9468  zneo  9494  xrlttri3  9939  qdceq  10409  flqltnz  10452  seqf1oglem1  10686  nn0opthd  10889  hashdifpr  10987  cats1un  11197  sumtp  11800  nninfctlemfo  12436  isprm2lem  12513  oddprm  12657  pcmpt  12741  ennnfonelemex  12860  perfectlem2  15547  lgsneg  15576  lgseisenlem4  15625  lgsquadlem1  15629  lgsquadlem3  15631  lgsquad2  15635  2lgsoddprm  15665  funvtxval0d  15707