Theorem necomd 2506

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

This proof depends on syntax axioms:   -> wi 4   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  ifnefals  3685  difsnb  3858  0nelop  4390  frecabcl  6675  fidifsnen  7178  tpfidisj  7242  omp1eomlem  7440  difinfsnlem  7445  fodjuomnilemdc  7490  en2eleq  7553  en2other2  7554  netap  7626  2omotaplemap  7629  ltned  8446  lt0ne0  8763  zdceq  9729  zneo  9757  xrlttri3  10215  qdceq  10695  flqltnz  10742  seqf1oglem1  10976  nn0opthd  11181  hashdifpr  11282  hashtpgim  11318  cats1un  11514  sumtp  12205  nninfctlemfo  12841  isprm2lem  12918  oddprm  13066  pcmpt  13150  ennnfonelemex  13362  psrridmfi  15209  perfectlem2  16317  lgsneg  16365  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem3  16420  lgsquad2  16424  2lgsoddprm  16454  funvtxval0d  16496  umgrvad2edg  16674  1hegrvtxdg1rfi  16773  vdegp1bid  16778  umgr2cwwk2dif  16887  eupth2lem3lem4fi  16936  pw1ndom3lem  17241  pw1ndom3  17242