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  3600  difsnb  3762  0nelop  4278  frecabcl  6454  fidifsnen  6928  tpfidisj  6986  omp1eomlem  7155  difinfsnlem  7160  fodjuomnilemdc  7205  en2eleq  7257  en2other2  7258  netap  7316  2omotaplemap  7319  ltned  8135  lt0ne0  8449  zdceq  9395  zneo  9421  xrlttri3  9866  qdceq  10317  flqltnz  10359  seqf1oglem1  10593  nn0opthd  10796  hashdifpr  10894  sumtp  11560  nninfctlemfo  12180  isprm2lem  12257  oddprm  12400  pcmpt  12484  ennnfonelemex  12574  lgsneg  15181  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem3  15236  lgsquad2  15240  2lgsoddprm  15270