Theorem necomd 2433

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

Syntax hints:   → wi 4   ≠ wne 2347

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  difsnb  3737  0nelop  4250  frecabcl  6403  fidifsnen  6873  tpfidisj  6930  omp1eomlem  7096  difinfsnlem  7101  fodjuomnilemdc  7145  en2eleq  7197  en2other2  7198  netap  7256  2omotaplemap  7259  ltned  8074  lt0ne0  8388  zdceq  9331  zneo  9357  xrlttri3  9800  qdceq  10250  flqltnz  10290  nn0opthd  10705  hashdifpr  10803  sumtp  11425  isprm2lem  12119  oddprm  12262  pcmpt  12344  ennnfonelemex  12418  lgsneg  14586