Theorem necomd 2506

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

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  4388  frecabcl  6670  fidifsnen  7172  tpfidisj  7236  omp1eomlem  7435  difinfsnlem  7440  fodjuomnilemdc  7485  en2eleq  7548  en2other2  7549  netap  7621  2omotaplemap  7624  ltned  8441  lt0ne0  8758  zdceq  9725  zneo  9752  xrlttri3  10210  qdceq  10690  flqltnz  10737  seqf1oglem1  10971  nn0opthd  11176  hashdifpr  11277  hashtpgim  11313  cats1un  11509  sumtp  12200  nninfctlemfo  12836  isprm2lem  12913  oddprm  13061  pcmpt  13145  ennnfonelemex  13357  perfectlem2  16266  lgsneg  16314  lgseisenlem4  16363  lgsquadlem1  16367  lgsquadlem3  16369  lgsquad2  16373  2lgsoddprm  16403  funvtxval0d  16445  umgrvad2edg  16623  1hegrvtxdg1rfi  16722  vdegp1bid  16727  umgr2cwwk2dif  16836  eupth2lem3lem4fi  16885  pw1ndom3lem  17190  pw1ndom3  17191