Theorem necom 2444

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 2191	. 2 |- ( A = B <-> B = A )
2	1	necon3bii 2398	1 |- ( A =/= B <-> B =/= A )

Syntax hints:   <-> wb 105   =/= wne 2360

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 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-ne 2361

This theorem is referenced by:  necomi  2445  necomd  2446  difprsn1  3746  difprsn2  3747  diftpsn3  3748  fndmdifcom  5643  fvpr1  5741  fvpr2  5742  fvpr1g  5743  fvtp1g  5745  fvtp2g  5746  fvtp3g  5747  fvtp2  5749  fvtp3  5750  netap  7283  2omotaplemap  7286  zltlen  9361  nn0lt2  9364  qltlen  9670  fzofzim  10218  flqeqceilz  10349  isprm2lem  12148  prm2orodd  12158  tridceq  15266