Theorem necom 2460

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

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

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 1470  ax-gen 1472  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-ne 2377

This theorem is referenced by:  necomi  2461  necomd  2462  difprsn1  3772  difprsn2  3773  diftpsn3  3774  fndmdifcom  5686  fvpr1  5788  fvpr2  5789  fvpr1g  5790  fvtp1g  5792  fvtp2g  5793  fvtp3g  5794  fvtp2  5796  fvtp3  5797  netap  7366  2omotaplemap  7369  zltlen  9451  nn0lt2  9454  qltlen  9761  fzofzim  10312  flqeqceilz  10463  isprm2lem  12438  prm2orodd  12448  tridceq  15995