Theorem necom 2335

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

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

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 577  ax-in2 578  ax-5 1379  ax-gen 1381  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-ne 2252

This theorem is referenced by:  necomi  2336  necomd  2337  difprsn1  3559  difprsn2  3560  diftpsn3  3561  fndmdifcom  5368  fvpr1  5462  fvpr2  5463  fvpr1g  5464  fvtp1g  5466  fvtp2g  5467  fvtp3g  5468  fvtp2  5470  fvtp3  5471  zltlen  8758  nn0lt2  8761  qltlen  9057  fzofzim  9527  flqeqceilz  9653  isprm2lem  10980  prm2orodd  10990