Theorem necomd 2500

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

Syntax hints:   → wi 4   ≠ wne 2414

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 1496  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  ifnefals  3671  difsnb  3842  0nelop  4369  frecabcl  6643  fidifsnen  7138  tpfidisj  7202  omp1eomlem  7398  difinfsnlem  7403  fodjuomnilemdc  7448  en2eleq  7511  en2other2  7512  netap  7584  2omotaplemap  7587  ltned  8403  lt0ne0  8720  zdceq  9673  zneo  9700  xrlttri3  10152  qdceq  10631  flqltnz  10674  seqf1oglem1  10908  nn0opthd  11112  hashdifpr  11213  hashtpgim  11245  cats1un  11441  sumtp  12128  nninfctlemfo  12764  isprm2lem  12841  oddprm  12985  pcmpt  13069  ennnfonelemex  13252  perfectlem2  15997  lgsneg  16026  lgseisenlem4  16075  lgsquadlem1  16079  lgsquadlem3  16081  lgsquad2  16085  2lgsoddprm  16115  funvtxval0d  16157  umgrvad2edg  16335  1hegrvtxdg1rfi  16434  vdegp1bid  16439  umgr2cwwk2dif  16548  eupth2lem3lem4fi  16597  pw1ndom3lem  16902  pw1ndom3  16903