Theorem necomd 2498

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

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

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  ifnefals  3667  difsnb  3837  0nelop  4364  frecabcl  6630  fidifsnen  7125  tpfidisj  7189  omp1eomlem  7385  difinfsnlem  7390  fodjuomnilemdc  7435  en2eleq  7498  en2other2  7499  netap  7568  2omotaplemap  7571  ltned  8387  lt0ne0  8702  zdceq  9653  zneo  9679  xrlttri3  10130  qdceq  10604  flqltnz  10647  seqf1oglem1  10881  nn0opthd  11084  hashdifpr  11185  hashtpgim  11217  cats1un  11413  sumtp  12100  nninfctlemfo  12736  isprm2lem  12813  oddprm  12957  pcmpt  13041  ennnfonelemex  13165  perfectlem2  15868  lgsneg  15897  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem3  15952  lgsquad2  15956  2lgsoddprm  15986  funvtxval0d  16028  umgrvad2edg  16206  1hegrvtxdg1rfi  16305  vdegp1bid  16310  umgr2cwwk2dif  16419  eupth2lem3lem4fi  16468  pw1ndom3lem  16763  pw1ndom3  16764