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 )

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

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced by:  ifnefals  3682  difsnb  3853  0nelop  4383  frecabcl  6660  fidifsnen  7162  tpfidisj  7226  omp1eomlem  7424  difinfsnlem  7429  fodjuomnilemdc  7474  en2eleq  7537  en2other2  7538  netap  7610  2omotaplemap  7613  ltned  8429  lt0ne0  8746  zdceq  9699  zneo  9726  xrlttri3  10178  qdceq  10657  flqltnz  10700  seqf1oglem1  10934  nn0opthd  11138  hashdifpr  11239  hashtpgim  11275  cats1un  11471  sumtp  12159  nninfctlemfo  12795  isprm2lem  12872  oddprm  13016  pcmpt  13100  ennnfonelemex  13283  perfectlem2  16028  lgsneg  16057  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem3  16112  lgsquad2  16116  2lgsoddprm  16146  funvtxval0d  16188  umgrvad2edg  16366  1hegrvtxdg1rfi  16465  vdegp1bid  16470  umgr2cwwk2dif  16579  eupth2lem3lem4fi  16628  pw1ndom3lem  16933  pw1ndom3  16934