Theorem necom 2487

Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)

Assertion

Ref	Expression
necom	⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 2233	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3bii 2441	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Syntax hints:   ↔ wb 105   ≠ wne 2403

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2404

This theorem is referenced by:  necomi  2488  necomd  2489  difprsn1  3817  difprsn2  3818  diftpsn3  3819  fndmdifcom  5762  fvpr1  5866  fvpr2  5867  fvpr1g  5868  fvtp1g  5870  fvtp2g  5871  fvtp3g  5872  fvtp2  5874  fvtp3  5875  netap  7516  2omotaplemap  7519  zltlen  9601  nn0lt2  9604  qltlen  9917  fzofzim  10471  flqeqceilz  10624  isprm2lem  12749  prm2orodd  12759  tridceq  16769