Theorem necomd 2506

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

This proof depends on syntax axioms:   -> wi 4   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  ifnefals  3685  difsnb  3858  0nelop  4388  frecabcl  6670  fidifsnen  7172  tpfidisj  7236  omp1eomlem  7435  difinfsnlem  7440  fodjuomnilemdc  7485  en2eleq  7548  en2other2  7549  netap  7621  2omotaplemap  7624  ltned  8441  lt0ne0  8758  zdceq  9725  zneo  9752  xrlttri3  10210  qdceq  10690  flqltnz  10737  seqf1oglem1  10971  nn0opthd  11176  hashdifpr  11277  hashtpgim  11313  cats1un  11509  sumtp  12200  nninfctlemfo  12836  isprm2lem  12913  oddprm  13061  pcmpt  13145  ennnfonelemex  13357  perfectlem2  16261  lgsneg  16309  lgseisenlem4  16358  lgsquadlem1  16362  lgsquadlem3  16364  lgsquad2  16368  2lgsoddprm  16398  funvtxval0d  16440  umgrvad2edg  16618  1hegrvtxdg1rfi  16717  vdegp1bid  16722  umgr2cwwk2dif  16831  eupth2lem3lem4fi  16880  pw1ndom3lem  17185  pw1ndom3  17186