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  7276  en2other2  7277  netap  7339  2omotaplemap  7342  ltned  8159  lt0ne0  8474  zdceq  9420  zneo  9446  xrlttri3  9891  qdceq  10353  flqltnz  10396  seqf1oglem1  10630  nn0opthd  10833  hashdifpr  10931  sumtp  11598  nninfctlemfo  12234  isprm2lem  12311  oddprm  12455  pcmpt  12539  ennnfonelemex  12658  perfectlem2  15322  lgsneg  15351  lgseisenlem4  15400  lgsquadlem1  15404  lgsquadlem3  15406  lgsquad2  15410  2lgsoddprm  15440