Theorem necom 2504

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

This proof depends on syntax axioms:   <-> wb 105   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  necomi  2505  necomd  2506  difprsn1  3854  difprsn2  3855  diftpsn3  3856  fndmdifcom  5818  fvpr1  5922  fvpr2  5923  fvpr1g  5924  fvtp1g  5926  fvtp2g  5927  fvtp3g  5928  fvtp2  5930  fvtp3  5931  netap  7626  2omotaplemap  7629  zltlen  9735  nn0lt2  9738  qltlen  10056  fzofzim  10617  flqeqceilz  10776  isprm2lem  12919  prm2orodd  12929  tridceq  17313