Theorem necomd 2466

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

Syntax hints:   → wi 4   ≠ wne 2380

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 1473  ax-gen 1475  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-ne 2381

This theorem is referenced by:  ifnefals  3627  difsnb  3790  0nelop  4313  frecabcl  6515  fidifsnen  7000  tpfidisj  7059  omp1eomlem  7229  difinfsnlem  7234  fodjuomnilemdc  7279  en2eleq  7341  en2other2  7342  netap  7408  2omotaplemap  7411  ltned  8228  lt0ne0  8543  zdceq  9490  zneo  9516  xrlttri3  9961  qdceq  10431  flqltnz  10474  seqf1oglem1  10708  nn0opthd  10911  hashdifpr  11009  cats1un  11219  sumtp  11891  nninfctlemfo  12527  isprm2lem  12604  oddprm  12748  pcmpt  12832  ennnfonelemex  12951  perfectlem2  15639  lgsneg  15668  lgseisenlem4  15717  lgsquadlem1  15721  lgsquadlem3  15723  lgsquad2  15727  2lgsoddprm  15757  funvtxval0d  15799  umgrvad2edg  15974