Theorem necom 2431

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

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

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  necomi  2432  necomd  2433  difprsn1  3731  difprsn2  3732  diftpsn3  3733  fndmdifcom  5622  fvpr1  5720  fvpr2  5721  fvpr1g  5722  fvtp1g  5724  fvtp2g  5725  fvtp3g  5726  fvtp2  5728  fvtp3  5729  netap  7252  2omotaplemap  7255  zltlen  9330  nn0lt2  9333  qltlen  9639  fzofzim  10187  flqeqceilz  10317  isprm2lem  12115  prm2orodd  12125  tridceq  14774