Theorem necomd 2453

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

Syntax hints:   → wi 4   ≠ wne 2367

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 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  ifnefals  3604  difsnb  3766  0nelop  4282  frecabcl  6466  fidifsnen  6940  tpfidisj  6999  omp1eomlem  7169  difinfsnlem  7174  fodjuomnilemdc  7219  en2eleq  7274  en2other2  7275  netap  7337  2omotaplemap  7340  ltned  8157  lt0ne0  8472  zdceq  9418  zneo  9444  xrlttri3  9889  qdceq  10351  flqltnz  10394  seqf1oglem1  10628  nn0opthd  10831  hashdifpr  10929  sumtp  11596  nninfctlemfo  12232  isprm2lem  12309  oddprm  12453  pcmpt  12537  ennnfonelemex  12656  perfectlem2  15320  lgsneg  15349  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem3  15404  lgsquad2  15408  2lgsoddprm  15438