Theorem necom 2424

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

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

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 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341

This theorem is referenced by:  necomi  2425  necomd  2426  difprsn1  3717  difprsn2  3718  diftpsn3  3719  fndmdifcom  5599  fvpr1  5697  fvpr2  5698  fvpr1g  5699  fvtp1g  5701  fvtp2g  5702  fvtp3g  5703  fvtp2  5705  fvtp3  5706  zltlen  9277  nn0lt2  9280  qltlen  9586  fzofzim  10131  flqeqceilz  10261  isprm2lem  12057  prm2orodd  12067  tridceq  14048