Theorem necom 1635

Description: Commutation of inequality.

Assertion

Ref	Expression
necom	|- (A =/= B <-> B =/= A)

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 1476	. 2 |- (A = B <-> B = A)
2	1	necon3bii 1597	1 |- (A =/= B <-> B =/= A)

Syntax hints:   <-> wb 146   =/= wne 1584

This theorem is referenced by:  necomd 1636  0pss 2306  0nep0 2734  orduniorsuc 3084  xp01disj 4140  kmlem3 4754  kmlem4 4755  leltnet 5508  xrltnrt 5528  nltmnft 5534  xrleltnet 5545  recgt0i 5784  geolimilem 7206  dscmet 7901  pilem1 8654  ch0psst 9357  efilcp 10539  efilcp2 10544  cnfilca 10545

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469  df-ne 1586

Copyright terms: Public domain