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  3735  0nelop  4246  frecabcl  6395  fidifsnen  6865  tpfidisj  6922  omp1eomlem  7088  difinfsnlem  7093  fodjuomnilemdc  7137  en2eleq  7189  en2other2  7190  netap  7248  2omotaplemap  7251  ltned  8065  lt0ne0  8379  zdceq  9322  zneo  9348  xrlttri3  9791  qdceq  10240  flqltnz  10280  nn0opthd  10693  hashdifpr  10791  sumtp  11413  isprm2lem  12106  oddprm  12249  pcmpt  12331  ennnfonelemex  12405  lgsneg  14207