Theorem necom 2451

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 105   ≠ wne 2367

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 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  necomi  2452  necomd  2453  difprsn1  3762  difprsn2  3763  diftpsn3  3764  fndmdifcom  5671  fvpr1  5769  fvpr2  5770  fvpr1g  5771  fvtp1g  5773  fvtp2g  5774  fvtp3g  5775  fvtp2  5777  fvtp3  5778  netap  7337  2omotaplemap  7340  zltlen  9421  nn0lt2  9424  qltlen  9731  fzofzim  10281  flqeqceilz  10427  isprm2lem  12309  prm2orodd  12319  tridceq  15787