Theorem necom 2392

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

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

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 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-ne 2309

This theorem is referenced by:  necomi  2393  necomd  2394  difprsn1  3659  difprsn2  3660  diftpsn3  3661  fndmdifcom  5526  fvpr1  5624  fvpr2  5625  fvpr1g  5626  fvtp1g  5628  fvtp2g  5629  fvtp3g  5630  fvtp2  5632  fvtp3  5633  zltlen  9129  nn0lt2  9132  qltlen  9432  fzofzim  9965  flqeqceilz  10091  isprm2lem  11797  prm2orodd  11807