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  7434  difinfsnlem  7439  fodjuomnilemdc  7484  en2eleq  7547  en2other2  7548  netap  7620  2omotaplemap  7623  ltned  8439  lt0ne0  8756  zdceq  9720  zneo  9747  xrlttri3  10199  qdceq  10679  flqltnz  10722  seqf1oglem1  10956  nn0opthd  11160  hashdifpr  11261  hashtpgim  11297  cats1un  11493  sumtp  12181  nninfctlemfo  12817  isprm2lem  12894  oddprm  13038  pcmpt  13122  ennnfonelemex  13305  perfectlem2  16114  lgsneg  16143  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem3  16198  lgsquad2  16202  2lgsoddprm  16232  funvtxval0d  16274  umgrvad2edg  16452  1hegrvtxdg1rfi  16551  vdegp1bid  16556  umgr2cwwk2dif  16665  eupth2lem3lem4fi  16714  pw1ndom3lem  17019  pw1ndom3  17020