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  8440  lt0ne0  8757  zdceq  9724  zneo  9751  xrlttri3  10209  qdceq  10689  flqltnz  10735  seqf1oglem1  10969  nn0opthd  11174  hashdifpr  11275  hashtpgim  11311  cats1un  11507  sumtp  12197  nninfctlemfo  12833  isprm2lem  12910  oddprm  13058  pcmpt  13142  ennnfonelemex  13354  perfectlem2  16198  lgsneg  16241  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem3  16296  lgsquad2  16300  2lgsoddprm  16330  funvtxval0d  16372  umgrvad2edg  16550  1hegrvtxdg1rfi  16649  vdegp1bid  16654  umgr2cwwk2dif  16763  eupth2lem3lem4fi  16812  pw1ndom3lem  17117  pw1ndom3  17118