Theorem necomd 2433

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

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

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  difsnb  3736  0nelop  4249  frecabcl  6400  fidifsnen  6870  tpfidisj  6927  omp1eomlem  7093  difinfsnlem  7098  fodjuomnilemdc  7142  en2eleq  7194  en2other2  7195  netap  7253  2omotaplemap  7256  ltned  8071  lt0ne0  8385  zdceq  9328  zneo  9354  xrlttri3  9797  qdceq  10247  flqltnz  10287  nn0opthd  10702  hashdifpr  10800  sumtp  11422  isprm2lem  12116  oddprm  12259  pcmpt  12341  ennnfonelemex  12415  lgsneg  14428