Theorem necomd 2395

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

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

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 1424  ax-gen 1426  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-ne 2310

This theorem is referenced by:  difsnb  3671  0nelop  4178  frecabcl  6304  fidifsnen  6772  tpfidisj  6824  omp1eomlem  6987  difinfsnlem  6992  fodjuomnilemdc  7024  en2eleq  7068  en2other2  7069  ltned  7901  lt0ne0  8214  zdceq  9150  zneo  9176  xrlttri3  9613  qdceq  10055  flqltnz  10091  nn0opthd  10500  hashdifpr  10598  sumtp  11215  isprm2lem  11833  ennnfonelemex  11963