Theorem necom 2462

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

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

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 1471  ax-gen 1473  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-ne 2379

This theorem is referenced by:  necomi  2463  necomd  2464  difprsn1  3783  difprsn2  3784  diftpsn3  3785  fndmdifcom  5709  fvpr1  5811  fvpr2  5812  fvpr1g  5813  fvtp1g  5815  fvtp2g  5816  fvtp3g  5817  fvtp2  5819  fvtp3  5820  netap  7401  2omotaplemap  7404  zltlen  9486  nn0lt2  9489  qltlen  9796  fzofzim  10349  flqeqceilz  10500  isprm2lem  12553  prm2orodd  12563  tridceq  16197