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  3603  difsnb  3765  0nelop  4281  frecabcl  6457  fidifsnen  6931  tpfidisj  6990  omp1eomlem  7160  difinfsnlem  7165  fodjuomnilemdc  7210  en2eleq  7262  en2other2  7263  netap  7321  2omotaplemap  7324  ltned  8140  lt0ne0  8455  zdceq  9401  zneo  9427  xrlttri3  9872  qdceq  10334  flqltnz  10377  seqf1oglem1  10611  nn0opthd  10814  hashdifpr  10912  sumtp  11579  nninfctlemfo  12207  isprm2lem  12284  oddprm  12428  pcmpt  12512  ennnfonelemex  12631  perfectlem2  15236  lgsneg  15265  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem3  15320  lgsquad2  15324  2lgsoddprm  15354