Theorem necom 2390

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 104   ≠ wne 2306

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 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-ne 2307

This theorem is referenced by:  necomi  2391  necomd  2392  difprsn1  3654  difprsn2  3655  diftpsn3  3656  fndmdifcom  5519  fvpr1  5617  fvpr2  5618  fvpr1g  5619  fvtp1g  5621  fvtp2g  5622  fvtp3g  5623  fvtp2  5625  fvtp3  5626  zltlen  9122  nn0lt2  9125  qltlen  9425  fzofzim  9958  flqeqceilz  10084  isprm2lem  11786  prm2orodd  11796