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  3735  0nelop  4248  frecabcl  6399  fidifsnen  6869  tpfidisj  6926  omp1eomlem  7092  difinfsnlem  7097  fodjuomnilemdc  7141  en2eleq  7193  en2other2  7194  netap  7252  2omotaplemap  7255  ltned  8070  lt0ne0  8384  zdceq  9327  zneo  9353  xrlttri3  9796  qdceq  10246  flqltnz  10286  nn0opthd  10701  hashdifpr  10799  sumtp  11421  isprm2lem  12115  oddprm  12258  pcmpt  12340  ennnfonelemex  12414  lgsneg  14395