Theorem necomd 2413

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

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

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 1427  ax-gen 1429  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-ne 2328

This theorem is referenced by:  difsnb  3700  0nelop  4209  frecabcl  6347  fidifsnen  6816  tpfidisj  6873  omp1eomlem  7039  difinfsnlem  7044  fodjuomnilemdc  7088  en2eleq  7131  en2other2  7132  ltned  7991  lt0ne0  8304  zdceq  9240  zneo  9266  xrlttri3  9705  qdceq  10150  flqltnz  10190  nn0opthd  10600  hashdifpr  10698  sumtp  11315  isprm2lem  11997  oddprm  12138  ennnfonelemex  12185