Theorem necom 2424

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 104   ≠ wne 2340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341

This theorem is referenced by:  necomi  2425  necomd  2426  difprsn1  3719  difprsn2  3720  diftpsn3  3721  fndmdifcom  5602  fvpr1  5700  fvpr2  5701  fvpr1g  5702  fvtp1g  5704  fvtp2g  5705  fvtp3g  5706  fvtp2  5708  fvtp3  5709  zltlen  9290  nn0lt2  9293  qltlen  9599  fzofzim  10144  flqeqceilz  10274  isprm2lem  12070  prm2orodd  12080  tridceq  14088