Theorem necomd 2421

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1435  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-ne 2336

This theorem is referenced by:  difsnb  3715  0nelop  4225  frecabcl  6363  fidifsnen  6832  tpfidisj  6889  omp1eomlem  7055  difinfsnlem  7060  fodjuomnilemdc  7104  en2eleq  7147  en2other2  7148  ltned  8008  lt0ne0  8322  zdceq  9262  zneo  9288  xrlttri3  9729  qdceq  10178  flqltnz  10218  nn0opthd  10631  hashdifpr  10729  sumtp  11351  isprm2lem  12044  oddprm  12187  pcmpt  12269  ennnfonelemex  12343  lgsneg  13525