Theorem necomd 2450

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

Syntax hints:   → wi 4   ≠ wne 2364

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 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-ne 2365

This theorem is referenced by:  ifnefals  3599  difsnb  3761  0nelop  4277  frecabcl  6452  fidifsnen  6926  tpfidisj  6984  omp1eomlem  7153  difinfsnlem  7158  fodjuomnilemdc  7203  en2eleq  7255  en2other2  7256  netap  7314  2omotaplemap  7317  ltned  8133  lt0ne0  8447  zdceq  9392  zneo  9418  xrlttri3  9863  qdceq  10314  flqltnz  10356  seqf1oglem1  10590  nn0opthd  10793  hashdifpr  10891  sumtp  11557  nninfctlemfo  12177  isprm2lem  12254  oddprm  12397  pcmpt  12481  ennnfonelemex  12571  lgsneg  15140  lgseisenlem4  15189  lgsquadlem1  15191