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  5688  fvpr1  5790  fvpr2  5791  fvpr1g  5792  fvtp1g  5794  fvtp2g  5795  fvtp3g  5796  fvtp2  5798  fvtp3  5799  netap  7368  2omotaplemap  7371  zltlen  9453  nn0lt2  9456  qltlen  9763  fzofzim  10314  flqeqceilz  10465  isprm2lem  12471  prm2orodd  12481  tridceq  16032