Theorem necomd 2486

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 2484	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

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  3648  difsnb  3814  0nelop  4338  frecabcl  6560  fidifsnen  7052  tpfidisj  7116  omp1eomlem  7287  difinfsnlem  7292  fodjuomnilemdc  7337  en2eleq  7399  en2other2  7400  netap  7466  2omotaplemap  7469  ltned  8286  lt0ne0  8601  zdceq  9548  zneo  9574  xrlttri3  10025  qdceq  10497  flqltnz  10540  seqf1oglem1  10774  nn0opthd  10977  hashdifpr  11077  cats1un  11295  sumtp  11968  nninfctlemfo  12604  isprm2lem  12681  oddprm  12825  pcmpt  12909  ennnfonelemex  13028  perfectlem2  15717  lgsneg  15746  lgseisenlem4  15795  lgsquadlem1  15799  lgsquadlem3  15801  lgsquad2  15805  2lgsoddprm  15835  funvtxval0d  15877  umgrvad2edg  16055  1hegrvtxdg1rfi  16121  vdegp1bid  16126  umgr2cwwk2dif  16233  pw1ndom3lem  16538  pw1ndom3  16539