Theorem necom 2444

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 105   ≠ wne 2360

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 1458  ax-gen 1460  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-ne 2361

This theorem is referenced by:  necomi  2445  necomd  2446  difprsn1  3746  difprsn2  3747  diftpsn3  3748  fndmdifcom  5638  fvpr1  5736  fvpr2  5737  fvpr1g  5738  fvtp1g  5740  fvtp2g  5741  fvtp3g  5742  fvtp2  5744  fvtp3  5745  netap  7271  2omotaplemap  7274  zltlen  9349  nn0lt2  9352  qltlen  9658  fzofzim  10206  flqeqceilz  10336  isprm2lem  12134  prm2orodd  12144  tridceq  15189