Theorem necom 2496

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 105   ≠ wne 2412

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  necomi  2497  necomd  2498  difprsn1  3832  difprsn2  3833  diftpsn3  3834  fndmdifcom  5783  fvpr1  5887  fvpr2  5888  fvpr1g  5889  fvtp1g  5891  fvtp2g  5892  fvtp3g  5893  fvtp2  5895  fvtp3  5896  netap  7567  2omotaplemap  7570  zltlen  9655  nn0lt2  9658  qltlen  9971  fzofzim  10526  flqeqceilz  10679  isprm2lem  12809  prm2orodd  12819  tridceq  16833