Theorem necom 2504

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

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

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  necomi  2505  necomd  2506  difprsn1  3852  difprsn2  3853  diftpsn3  3854  fndmdifcom  5809  fvpr1  5913  fvpr2  5914  fvpr1g  5915  fvtp1g  5917  fvtp2g  5918  fvtp3g  5919  fvtp2  5921  fvtp3  5922  netap  7614  2omotaplemap  7617  zltlen  9707  nn0lt2  9710  qltlen  10023  fzofzim  10583  flqeqceilz  10738  isprm2lem  12877  prm2orodd  12887  tridceq  17080