Theorem necomd 2461

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

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

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 1469  ax-gen 1471  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-ne 2376

This theorem is referenced by:  ifnefals  3613  difsnb  3775  0nelop  4291  frecabcl  6484  fidifsnen  6966  tpfidisj  7025  omp1eomlem  7195  difinfsnlem  7200  fodjuomnilemdc  7245  en2eleq  7302  en2other2  7303  netap  7365  2omotaplemap  7368  ltned  8185  lt0ne0  8500  zdceq  9447  zneo  9473  xrlttri3  9918  qdceq  10385  flqltnz  10428  seqf1oglem1  10662  nn0opthd  10865  hashdifpr  10963  sumtp  11667  nninfctlemfo  12303  isprm2lem  12380  oddprm  12524  pcmpt  12608  ennnfonelemex  12727  perfectlem2  15414  lgsneg  15443  lgseisenlem4  15492  lgsquadlem1  15496  lgsquadlem3  15498  lgsquad2  15502  2lgsoddprm  15532  funvtxval0d  15572