Theorem necom 2283

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

Assertion

Ref	Expression
necom	⊢ (A ≠ B ↔ B ≠ A)

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 2039	. 2 ⊢ (A = B ↔ B = A)
2	1	necon3bii 2237	1 ⊢ (A ≠ B ↔ B ≠ A)

Syntax hints:   ↔ wb 98   ≠ wne 2201

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-5 1333  ax-gen 1335  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-ne 2203

This theorem is referenced by:  necomi  2284  necomd  2285  0pss  3259  difprsn1  3494  difprsn2  3495  diftpsn3  3496  fndmdifcom  5216  fvpr1  5308  fvpr2  5309  fvpr1g  5310  fvtp1g  5312  fvtp2g  5313  fvtp3g  5314  fvtp2  5316  fvtp3  5317  zltlen  8095  nn0lt2  8098  fzofzim  8814