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 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ≠ wne 2420

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  ifnefals  3685  difsnb  3856  0nelop  4386  frecabcl  6664  fidifsnen  7166  tpfidisj  7230  omp1eomlem  7428  difinfsnlem  7433  fodjuomnilemdc  7478  en2eleq  7541  en2other2  7542  netap  7614  2omotaplemap  7617  ltned  8433  lt0ne0  8750  zdceq  9703  zneo  9730  xrlttri3  10182  qdceq  10662  flqltnz  10705  seqf1oglem1  10939  nn0opthd  11143  hashdifpr  11244  hashtpgim  11280  cats1un  11476  sumtp  12164  nninfctlemfo  12800  isprm2lem  12877  oddprm  13021  pcmpt  13105  ennnfonelemex  13288  perfectlem2  16097  lgsneg  16126  lgseisenlem4  16175  lgsquadlem1  16179  lgsquadlem3  16181  lgsquad2  16185  2lgsoddprm  16215  funvtxval0d  16257  umgrvad2edg  16435  1hegrvtxdg1rfi  16534  vdegp1bid  16539  umgr2cwwk2dif  16648  eupth2lem3lem4fi  16697  pw1ndom3lem  17002  pw1ndom3  17003