Theorem necom 2329

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

Syntax hints:   <-> wb 103   =/= wne 2245

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-5 1376  ax-gen 1378  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-ne 2246

This theorem is referenced by:  necomi  2330  necomd  2331  difprsn1  3525  difprsn2  3526  diftpsn3  3527  fndmdifcom  5294  fvpr1  5386  fvpr2  5387  fvpr1g  5388  fvtp1g  5390  fvtp2g  5391  fvtp3g  5392  fvtp2  5394  fvtp3  5395  zltlen  8426  nn0lt2  8429  qltlen  8725  fzofzim  9197  flqeqceilz  9320  isprm2lem  10498  prm2orodd  10508