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  3732  difprsn2  3733  diftpsn3  3734  fndmdifcom  5623  fvpr1  5721  fvpr2  5722  fvpr1g  5723  fvtp1g  5725  fvtp2g  5726  fvtp3g  5727  fvtp2  5729  fvtp3  5730  netap  7253  2omotaplemap  7256  zltlen  9331  nn0lt2  9334  qltlen  9640  fzofzim  10188  flqeqceilz  10318  isprm2lem  12116  prm2orodd  12126  tridceq  14807