Theorem necom 2461

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 105   ≠ wne 2377

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 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-ne 2378

This theorem is referenced by:  necomi  2462  necomd  2463  difprsn1  3777  difprsn2  3778  diftpsn3  3779  fndmdifcom  5698  fvpr1  5800  fvpr2  5801  fvpr1g  5802  fvtp1g  5804  fvtp2g  5805  fvtp3g  5806  fvtp2  5808  fvtp3  5809  netap  7381  2omotaplemap  7384  zltlen  9466  nn0lt2  9469  qltlen  9776  fzofzim  10329  flqeqceilz  10480  isprm2lem  12508  prm2orodd  12518  tridceq  16130