Theorem necom 2504

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

Assertion

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

Proof of Theorem necom

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

This proof depends on syntax axioms:   ↔ wb 105   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  necomi  2505  necomd  2506  difprsn1  3854  difprsn2  3855  diftpsn3  3856  fndmdifcom  5815  fvpr1  5919  fvpr2  5920  fvpr1g  5921  fvtp1g  5923  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  netap  7620  2omotaplemap  7623  zltlen  9726  nn0lt2  9729  qltlen  10042  fzofzim  10602  flqeqceilz  10757  isprm2lem  12896  prm2orodd  12906  tridceq  17118