Theorem necom 2393

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

Syntax hints:   <-> wb 104   =/= wne 2309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1424  ax-gen 1426  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-ne 2310

This theorem is referenced by:  necomi  2394  necomd  2395  difprsn1  3667  difprsn2  3668  diftpsn3  3669  fndmdifcom  5534  fvpr1  5632  fvpr2  5633  fvpr1g  5634  fvtp1g  5636  fvtp2g  5637  fvtp3g  5638  fvtp2  5640  fvtp3  5641  zltlen  9153  nn0lt2  9156  qltlen  9459  fzofzim  9996  flqeqceilz  10122  isprm2lem  11833  prm2orodd  11843