Theorem necom 2484

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 105   ≠ wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  necomi  2485  necomd  2486  difprsn1  3807  difprsn2  3808  diftpsn3  3809  fndmdifcom  5743  fvpr1  5847  fvpr2  5848  fvpr1g  5849  fvtp1g  5851  fvtp2g  5852  fvtp3g  5853  fvtp2  5855  fvtp3  5856  netap  7448  2omotaplemap  7451  zltlen  9533  nn0lt2  9536  qltlen  9843  fzofzim  10396  flqeqceilz  10548  isprm2lem  12646  prm2orodd  12656  tridceq  16454