Theorem necom 2451

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

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

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 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  necomi  2452  necomd  2453  difprsn1  3761  difprsn2  3762  diftpsn3  3763  fndmdifcom  5668  fvpr1  5766  fvpr2  5767  fvpr1g  5768  fvtp1g  5770  fvtp2g  5771  fvtp3g  5772  fvtp2  5774  fvtp3  5775  netap  7321  2omotaplemap  7324  zltlen  9404  nn0lt2  9407  qltlen  9714  fzofzim  10264  flqeqceilz  10410  isprm2lem  12284  prm2orodd  12294  tridceq  15700