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  4390  frecabcl  6674  fidifsnen  7176  tpfidisj  7240  omp1eomlem  7440  difinfsnlem  7445  fodjuomnilemdc  7490  en2eleq  7553  en2other2  7554  netap  7626  2omotaplemap  7629  ltned  8446  lt0ne0  8763  zdceq  9731  zneo  9758  xrlttri3  10216  qdceq  10696  flqltnz  10743  seqf1oglem1  10977  nn0opthd  11182  hashdifpr  11283  hashtpgim  11319  cats1un  11515  sumtp  12206  nninfctlemfo  12842  isprm2lem  12919  oddprm  13067  pcmpt  13151  ennnfonelemex  13363  psrridmfi  15200  perfectlem2  16300  lgsneg  16348  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem3  16403  lgsquad2  16407  2lgsoddprm  16437  funvtxval0d  16479  umgrvad2edg  16657  1hegrvtxdg1rfi  16756  vdegp1bid  16761  umgr2cwwk2dif  16870  eupth2lem3lem4fi  16919  pw1ndom3lem  17224  pw1ndom3  17225