Theorem necomd 2335

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-5 1377  ax-gen 1379  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-ne 2250

This theorem is referenced by:  difsnb  3548  0nelop  4031  frecabcl  6068  fidifsnen  6426  en2eleq  6573  en2other2  6574  ltned  7343  lt0ne0  7651  zdceq  8556  zneo  8581  xrlttri3  9000  qdceq  9385  flqltnz  9421  expival  9627  nn0opthd  9798  hashdifpr  9896  isprm2lem  10705