Theorem necomd 2487

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

Syntax hints:   → wi 4   ≠ wne 2401

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 2212

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-ne 2402

This theorem is referenced by:  ifnefals  3651  difsnb  3817  0nelop  4342  frecabcl  6570  fidifsnen  7062  tpfidisj  7126  omp1eomlem  7298  difinfsnlem  7303  fodjuomnilemdc  7348  en2eleq  7411  en2other2  7412  netap  7478  2omotaplemap  7481  ltned  8298  lt0ne0  8613  zdceq  9560  zneo  9586  xrlttri3  10037  qdceq  10510  flqltnz  10553  seqf1oglem1  10787  nn0opthd  10990  hashdifpr  11090  hashtpgim  11115  cats1un  11311  sumtp  11998  nninfctlemfo  12634  isprm2lem  12711  oddprm  12855  pcmpt  12939  ennnfonelemex  13058  perfectlem2  15753  lgsneg  15782  lgseisenlem4  15831  lgsquadlem1  15835  lgsquadlem3  15837  lgsquad2  15841  2lgsoddprm  15871  funvtxval0d  15913  umgrvad2edg  16091  1hegrvtxdg1rfi  16190  vdegp1bid  16195  umgr2cwwk2dif  16304  eupth2lem3lem4fi  16353  pw1ndom3lem  16648  pw1ndom3  16649