Theorem necom 2498

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 105   ≠ wne 2414

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  necomi  2499  necomd  2500  difprsn1  3838  difprsn2  3839  diftpsn3  3840  fndmdifcom  5789  fvpr1  5893  fvpr2  5894  fvpr1g  5895  fvtp1g  5897  fvtp2g  5898  fvtp3g  5899  fvtp2  5901  fvtp3  5902  netap  7584  2omotaplemap  7587  zltlen  9674  nn0lt2  9677  qltlen  9990  fzofzim  10549  flqeqceilz  10704  isprm2lem  12838  prm2orodd  12848  tridceq  16953