Theorem necom 2448

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

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

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 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-ne 2365

This theorem is referenced by:  necomi  2449  necomd  2450  difprsn1  3757  difprsn2  3758  diftpsn3  3759  fndmdifcom  5664  fvpr1  5762  fvpr2  5763  fvpr1g  5764  fvtp1g  5766  fvtp2g  5767  fvtp3g  5768  fvtp2  5770  fvtp3  5771  netap  7314  2omotaplemap  7317  zltlen  9395  nn0lt2  9398  qltlen  9705  fzofzim  10255  flqeqceilz  10389  isprm2lem  12254  prm2orodd  12264  tridceq  15546