Theorem necomd 2486

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

Syntax hints:   → wi 4   ≠ wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  ifnefals  3647  difsnb  3811  0nelop  4334  frecabcl  6551  fidifsnen  7040  tpfidisj  7099  omp1eomlem  7269  difinfsnlem  7274  fodjuomnilemdc  7319  en2eleq  7381  en2other2  7382  netap  7448  2omotaplemap  7451  ltned  8268  lt0ne0  8583  zdceq  9530  zneo  9556  xrlttri3  10001  qdceq  10472  flqltnz  10515  seqf1oglem1  10749  nn0opthd  10952  hashdifpr  11050  cats1un  11261  sumtp  11933  nninfctlemfo  12569  isprm2lem  12646  oddprm  12790  pcmpt  12874  ennnfonelemex  12993  perfectlem2  15682  lgsneg  15711  lgseisenlem4  15760  lgsquadlem1  15764  lgsquadlem3  15766  lgsquad2  15770  2lgsoddprm  15800  funvtxval0d  15842  umgrvad2edg  16017  pw1ndom3lem  16382  pw1ndom3  16383