Theorem necomd 2486

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

Syntax hints:   → wi 4   ≠ wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  ifnefals  3647  difsnb  3811  0nelop  4335  frecabcl  6556  fidifsnen  7045  tpfidisj  7107  omp1eomlem  7277  difinfsnlem  7282  fodjuomnilemdc  7327  en2eleq  7389  en2other2  7390  netap  7456  2omotaplemap  7459  ltned  8276  lt0ne0  8591  zdceq  9538  zneo  9564  xrlttri3  10010  qdceq  10481  flqltnz  10524  seqf1oglem1  10758  nn0opthd  10961  hashdifpr  11060  cats1un  11274  sumtp  11946  nninfctlemfo  12582  isprm2lem  12659  oddprm  12803  pcmpt  12887  ennnfonelemex  13006  perfectlem2  15695  lgsneg  15724  lgseisenlem4  15773  lgsquadlem1  15777  lgsquadlem3  15779  lgsquad2  15783  2lgsoddprm  15813  funvtxval0d  15855  umgrvad2edg  16030  umgr2cwwk2dif  16192  pw1ndom3lem  16466  pw1ndom3  16467