Theorem necomd 2498

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

Syntax hints:   → wi 4   ≠ wne 2412

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  ifnefals  3666  difsnb  3836  0nelop  4363  frecabcl  6629  fidifsnen  7124  tpfidisj  7188  omp1eomlem  7384  difinfsnlem  7389  fodjuomnilemdc  7434  en2eleq  7497  en2other2  7498  netap  7564  2omotaplemap  7567  ltned  8383  lt0ne0  8698  zdceq  9649  zneo  9675  xrlttri3  10126  qdceq  10600  flqltnz  10643  seqf1oglem1  10877  nn0opthd  11080  hashdifpr  11180  hashtpgim  11210  cats1un  11406  sumtp  12093  nninfctlemfo  12729  isprm2lem  12806  oddprm  12950  pcmpt  13034  ennnfonelemex  13154  perfectlem2  15855  lgsneg  15884  lgseisenlem4  15933  lgsquadlem1  15937  lgsquadlem3  15939  lgsquad2  15943  2lgsoddprm  15973  funvtxval0d  16015  umgrvad2edg  16193  1hegrvtxdg1rfi  16292  vdegp1bid  16297  umgr2cwwk2dif  16406  eupth2lem3lem4fi  16455  pw1ndom3lem  16750  pw1ndom3  16751