Theorem necomd 2488

Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)

Hypothesis

Ref	Expression
necomd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Assertion

Ref	Expression
necomd	⊢ (𝜑 → 𝐵 ≠ 𝐴)

Proof of Theorem necomd

Step	Hyp	Ref	Expression
1		necomd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		necom 2486	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ≠ wne 2402

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 1495  ax-gen 1497  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2403

This theorem is referenced by:  ifnefals  3650  difsnb  3816  0nelop  4340  frecabcl  6565  fidifsnen  7057  tpfidisj  7121  omp1eomlem  7293  difinfsnlem  7298  fodjuomnilemdc  7343  en2eleq  7406  en2other2  7407  netap  7473  2omotaplemap  7476  ltned  8293  lt0ne0  8608  zdceq  9555  zneo  9581  xrlttri3  10032  qdceq  10505  flqltnz  10548  seqf1oglem1  10782  nn0opthd  10985  hashdifpr  11085  cats1un  11303  sumtp  11977  nninfctlemfo  12613  isprm2lem  12690  oddprm  12834  pcmpt  12918  ennnfonelemex  13037  perfectlem2  15727  lgsneg  15756  lgseisenlem4  15805  lgsquadlem1  15809  lgsquadlem3  15811  lgsquad2  15815  2lgsoddprm  15845  funvtxval0d  15887  umgrvad2edg  16065  1hegrvtxdg1rfi  16164  vdegp1bid  16169  umgr2cwwk2dif  16278  eupth2lem3lem4fi  16327  pw1ndom3lem  16609  pw1ndom3  16610