Theorem necom 1636

Description: Commutation of inequality.

Assertion

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

Proof of Theorem necom

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

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

This theorem is referenced by:  necomd 1637  0pss 2308  0nep0 2737  orduniorsuc 3087  xp01disj 4143  kmlem3 4767  kmlem4 4768  leltnet 5521  xrltnrt 5541  nltmnft 5547  xrleltnet 5558  recgt0i 5814  nn0opth 6666  geolimilem 7235  dscmet 7918  pilem1 8671  ch0psst 9369  top2ind 10548  top2usne 10549  homindlem3 10551  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain