Theorem necom 3013

Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)

Assertion

Ref	Expression
necom	⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 2772	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3bii 3012	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Syntax hints:   ↔ wb 209   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  necomi  3014  necomd  3015  dfdif3  4074  0pss  4404  iftrueb  4496  disjtp2  4678  difprsn1  4763  difprsn2  4764  prproe  4866  fndmdifcom  7028  fvpr1g  7178  fvpr2g  7179  fvtp1  7183  fvtp2  7184  fvtp3  7185  fvtp1g  7186  fvtp2g  7187  fvtp3g  7188  dff14b  7259  f12dfv  7261  f13dfv  7262  orduniorsuc  7814  kmlem3  10124  kmlem4  10125  ac6num  10451  leltne  11287  nn0lt2  12650  xrleltne  13161  fzofzim  13729  elfznelfzo  13793  elfznelfzob  13794  fleqceilz  13878  hashdifpr  14442  hashgt12el  14449  hashgt12el2  14450  hashgt23el  14451  hash7g  14513  cshw0  14821  cshwn  14824  isprm2lem  16729  prm2orodd  16739  cshwsdisj  17148  sgrp2nmndlem5  18981  f1omvdconj  19507  pmtrprfv3  19515  pmtr3ncomlem1  19534  dmdprdd  20062  cnfldfunALT  21497  xrsdsreclblem  21523  xrsdsreclb  21524  ordthaus  23502  hmphindis  23915  angpined  26953  nosgnn0  27780  noextendlt  27791  nosepne  27802  nosepdm  27806  nosupbnd2lem1  27837  noinfbnd2lem1  27852  noetasuplem4  27858  funvtxval0  29274  snstrvtxval  29296  snstriedgval  29297  nbgrsym  29622  nb3grprlem2  29640  nb3grpr  29641  cusgredg  29683  cplgr3v  29694  1egrvtxdg0  29770  usgr2pthlem  30021  usgr2pth0  30023  2pthdlem1  30188  clwlkclwwlklem2a4  30257  uhgr3cyclex  30442  eupth2lem3lem4  30491  frcond1  30526  frcond4  30530  frgr3v  30535  3vfriswmgr  30538  2pthfrgr  30544  3cyclfrgrrn1  30545  n4cyclfrgr  30551  frgrnbnb  30553  frgrwopreglem4a  30570  ch0pss  31706  pmtrprfv2  33321  esumcvgre  34398  bnj563  35049  cusgredgex2  35486  cvmsdisj  35633  fmlaomn0  35753  ex-sategoelel  35784  btwnouttr  36387  fscgr  36443  linecom  36513  linerflx2  36514  mh-inf3f1  36914  poimirlem25  38156  divrngidl  38539  lcvbr3  39659  opltn0  39826  atlltn0  39942  2dim  40106  ps-2  40114  islln3  40146  llnexatN  40157  4atlem11  40245  isline4N  40413  lhpex2leN  40649  cdleme48gfv  41173  60gcd7e1  42634  dvrelogpow2b  42697  aks4d1p1p4  42700  aks6d1c2p2  42748  fsuppind  43184  onov0suclim  43863  oenassex  43907  pr2eldif2  44143  pimxrneun  46060  icccncfext  46459  fourierdlem42  46721  icceuelpartlem  48039  ichnreuop  48076  paireqne  48115  oddprmALTV  48307  rrx2pnedifcoorneor  49347  rrx2linest  49373