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  5669  fvpr1  5767  fvpr2  5768  fvpr1g  5769  fvtp1g  5771  fvtp2g  5772  fvtp3g  5773  fvtp2  5775  fvtp3  5776  netap  7323  2omotaplemap  7326  zltlen  9406  nn0lt2  9409  qltlen  9716  fzofzim  10266  flqeqceilz  10412  isprm2lem  12294  prm2orodd  12304  tridceq  15710