Theorem necomd 2486

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

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

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  ifnefals  3647  difsnb  3810  0nelop  4333  frecabcl  6543  fidifsnen  7028  tpfidisj  7087  omp1eomlem  7257  difinfsnlem  7262  fodjuomnilemdc  7307  en2eleq  7369  en2other2  7370  netap  7436  2omotaplemap  7439  ltned  8256  lt0ne0  8571  zdceq  9518  zneo  9544  xrlttri3  9989  qdceq  10459  flqltnz  10502  seqf1oglem1  10736  nn0opthd  10939  hashdifpr  11037  cats1un  11248  sumtp  11920  nninfctlemfo  12556  isprm2lem  12633  oddprm  12777  pcmpt  12861  ennnfonelemex  12980  perfectlem2  15668  lgsneg  15697  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem3  15752  lgsquad2  15756  2lgsoddprm  15786  funvtxval0d  15828  umgrvad2edg  16003