Theorem necom 2431

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 105   ≠ wne 2347

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  necomi  2432  necomd  2433  difprsn1  3733  difprsn2  3734  diftpsn3  3735  fndmdifcom  5624  fvpr1  5722  fvpr2  5723  fvpr1g  5724  fvtp1g  5726  fvtp2g  5727  fvtp3g  5728  fvtp2  5730  fvtp3  5731  netap  7255  2omotaplemap  7258  zltlen  9333  nn0lt2  9336  qltlen  9642  fzofzim  10190  flqeqceilz  10320  isprm2lem  12118  prm2orodd  12128  tridceq  14889