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  5815  fvpr1  5919  fvpr2  5920  fvpr1g  5921  fvtp1g  5923  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  netap  7620  2omotaplemap  7623  zltlen  9724  nn0lt2  9727  qltlen  10040  fzofzim  10600  flqeqceilz  10755  isprm2lem  12894  prm2orodd  12904  tridceq  17110