Theorem necomd 2422

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

Syntax hints:   → wi 4   ≠ wne 2336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1435  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-ne 2337

This theorem is referenced by:  difsnb  3716  0nelop  4226  frecabcl  6367  fidifsnen  6836  tpfidisj  6893  omp1eomlem  7059  difinfsnlem  7064  fodjuomnilemdc  7108  en2eleq  7151  en2other2  7152  ltned  8012  lt0ne0  8326  zdceq  9266  zneo  9292  xrlttri3  9733  qdceq  10182  flqltnz  10222  nn0opthd  10635  hashdifpr  10733  sumtp  11355  isprm2lem  12048  oddprm  12191  pcmpt  12273  ennnfonelemex  12347  lgsneg  13565