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  4390  frecabcl  6674  fidifsnen  7177  tpfidisj  7241  omp1eomlem  7441  difinfsnlem  7446  fodjuomnilemdc  7491  en2eleq  7554  en2other2  7555  netap  7627  2omotaplemap  7630  ltned  8447  lt0ne0  8764  zdceq  9732  zneo  9759  xrlttri3  10217  qdceq  10697  flqltnz  10744  seqf1oglem1  10978  nn0opthd  11183  hashdifpr  11284  hashtpgim  11320  cats1un  11516  sumtp  12207  nninfctlemfo  12843  isprm2lem  12920  oddprm  13068  pcmpt  13152  ennnfonelemex  13364  psrridmfi  15205  perfectlem2  16312  lgsneg  16360  lgseisenlem4  16409  lgsquadlem1  16413  lgsquadlem3  16415  lgsquad2  16419  2lgsoddprm  16449  funvtxval0d  16491  umgrvad2edg  16669  1hegrvtxdg1rfi  16768  vdegp1bid  16773  umgr2cwwk2dif  16882  eupth2lem3lem4fi  16931  pw1ndom3lem  17236  pw1ndom3  17237