Theorem necomd 2426

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

Syntax hints:   → wi 4   ≠ wne 2340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341

This theorem is referenced by:  difsnb  3723  0nelop  4233  frecabcl  6378  fidifsnen  6848  tpfidisj  6905  omp1eomlem  7071  difinfsnlem  7076  fodjuomnilemdc  7120  en2eleq  7172  en2other2  7173  ltned  8033  lt0ne0  8347  zdceq  9287  zneo  9313  xrlttri3  9754  qdceq  10203  flqltnz  10243  nn0opthd  10656  hashdifpr  10755  sumtp  11377  isprm2lem  12070  oddprm  12213  pcmpt  12295  ennnfonelemex  12369  lgsneg  13719