Theorem necomd 2394

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

Syntax hints:   → wi 4   ≠ wne 2308

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 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-ne 2309

This theorem is referenced by:  difsnb  3663  0nelop  4170  frecabcl  6296  fidifsnen  6764  tpfidisj  6816  omp1eomlem  6979  difinfsnlem  6984  fodjuomnilemdc  7016  en2eleq  7051  en2other2  7052  ltned  7877  lt0ne0  8190  zdceq  9126  zneo  9152  xrlttri3  9583  qdceq  10024  flqltnz  10060  nn0opthd  10468  hashdifpr  10566  sumtp  11183  isprm2lem  11797  ennnfonelemex  11927