Theorem necom 2420

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 104   ≠ wne 2336

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 604  ax-in2 605  ax-5 1435  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-ne 2337

This theorem is referenced by:  necomi  2421  necomd  2422  difprsn1  3712  difprsn2  3713  diftpsn3  3714  fndmdifcom  5591  fvpr1  5689  fvpr2  5690  fvpr1g  5691  fvtp1g  5693  fvtp2g  5694  fvtp3g  5695  fvtp2  5697  fvtp3  5698  zltlen  9269  nn0lt2  9272  qltlen  9578  fzofzim  10123  flqeqceilz  10253  isprm2lem  12048  prm2orodd  12058  tridceq  13935